mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.coe_symm : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} (φ : ρ.Equiv σ),
  ⇑(↑φ.toContinuousLinearEquiv).symm = ⇑φ.symm
-- Mathlib.Lean.MessageData.ForExprs
Lean.MessageData.instForInExprsProdPPContextExpr : {m : Type → Type u} → [Monad m] → [MonadLiftT BaseIO m] → ForIn m Lean.MessageData.Exprs (Lean.PPContext × Lean.Expr)
-- Lean.Meta.Tactic.Backtrack
/-- * `n : Nat` steps remaining.
* `curr : List MVarId` the current list of unsolved goals.
* `acc : List MVarId` a list of "suspended" goals, which will be returned as subgoals.
 -/
_private.Lean.Meta.Tactic.Backtrack.0.Lean.Meta.Tactic.Backtrack.Backtrack.run : Lean.Meta.Tactic.Backtrack.BacktrackConfig →
  optParam Lean.Name Lean.Name.anonymous →
    (Lean.MVarId → (List Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))) → Lean.MetaM (List Lean.MVarId)) →
      List Lean.MVarId → ℕ → List Lean.MVarId → List Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Batteries.Data.Fin.Lemmas
Fin.divNat_mkDivMod_modNat : ∀ {m n : ℕ} (k : Fin (m * n)), k.divNat.mkDivMod k.modNat = k
-- Mathlib.Algebra.Algebra.Operations
Submodule.comap_unop_mul : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] (M N : Submodule R A),
  Submodule.comap (↑(MulOpposite.opLinearEquiv R).symm) (M * N) =
    Submodule.comap (↑(MulOpposite.opLinearEquiv R).symm) N * Submodule.comap (↑(MulOpposite.opLinearEquiv R).symm) M
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeft_obj_hom : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  {L₁ L₂ : CategoryTheory.Functor A T} (l : L₁ ⟶ L₂) (X : CategoryTheory.Comma L₂ R),
  ((CategoryTheory.Comma.mapLeft R l).obj X).hom = CategoryTheory.CategoryStruct.comp (l.app X.left) X.hom
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsAtomic.castLE : ∀ {L : FirstOrder.Language} {α : Type u'} {n l : ℕ} {φ : L.BoundedFormula α l} {h : l ≤ n},
  φ.IsAtomic → (FirstOrder.Language.BoundedFormula.castLE h φ).IsAtomic
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.contains_eq_isSome_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {a : α}, t.contains a = (Std.ExtDTreeMap.Const.get? t a).isSome
-- Mathlib.Analysis.Calculus.UniformLimitsDeriv
uniformCauchySeqOn_ball_of_deriv : ∀ {ι : Type u_1} {l : Filter ι} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {G : Type u_3}
  [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G] {f f' : ι → 𝕜 → G} {x : 𝕜} [IsRCLikeNormedField 𝕜] {r : ℝ},
  UniformCauchySeqOn f' l (Metric.ball x r) →
    (∀ (n : ι), ∀ y ∈ Metric.ball x r, HasDerivAt (f n) (f' n y) y) →
      Cauchy (Filter.map (fun n => f n x) l) → UniformCauchySeqOn f l (Metric.ball x r)
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.opId_hom_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X : Cᵒᵖ),
  (CategoryTheory.Functor.opId C).hom.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.RingTheory.Etale.Field
Algebra.FormallyEtale.equivPiOfIsSepClosed_self_apply : ∀ {K : Type u_1} [inst : Field K] [inst_1 : IsSepClosed K] (x : K) (p : PrimeSpectrum K),
  (Algebra.FormallyEtale.equivPiOfIsSepClosed K K) x p = x
-- Mathlib.Topology.Compactness.Compact
/-- If `f : X → Y` is an embedding, the image `f '' s` of a set `s` is compact
if and only if `s` is compact.  -/
Topology.IsEmbedding.isCompact_iff : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {f : X → Y},
  Topology.IsEmbedding f → (IsCompact s ↔ IsCompact (f '' s))
-- Mathlib.Data.Set.Function
Set.SurjOn.mapsTo_invFunOn : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} [inst : Nonempty α],
  Set.SurjOn f s t → Set.MapsTo (Function.invFunOn f s) t s
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverMincard_monotone_time : ∀ {X : Type u_1} (T : X → X) (F : Set X) (U : SetRel X X), Monotone fun n => Dynamics.coverMincard T F U n
-- Mathlib.Order.SuccPred.IntervalSucc
/-- If `α` is a linear succ order, `β` is a preorder, and `f : α → β` is a monotone function, then
the intervals `Set.Ico (f n) (f (Order.succ n))` are pairwise disjoint.  -/
Monotone.pairwise_disjoint_on_Ico_succ : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : Preorder β] {f : α → β},
  Monotone f → Pairwise (Function.onFun Disjoint fun n => Set.Ico (f n) (f (Order.succ n)))
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.setRoot.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (h_1 : Unit → motive RBTree.RBNode.nil)
  (h_2 :
    (c : RBTree.RBColor) →
      (a : RBTree.RBNode α) → (v : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node c a v b)),
  (match RBTree.RBNode.nil with
    | RBTree.RBNode.nil => h_1 ()
    | RBTree.RBNode.node c a v b => h_2 c a v b) =
    h_1 ()
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleConfig.ruleSets : Aesop.Frontend.RuleConfig → Aesop.Frontend.RuleSets
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.iterate_derivative_T_eval_one_recurrence : ∀ {R : Type u_1} [inst : CommRing R] (n : ℤ) (k : ℕ),
  (2 * ↑k + 1) * Polynomial.eval 1 ((⇑Polynomial.derivative)^[k + 1] (Polynomial.Chebyshev.T R n)) =
    (↑n ^ 2 - ↑k ^ 2) * Polynomial.eval 1 ((⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.T R n))
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.card_le_nat : ∀ {o : Ordinal.{u_1}} {n : ℕ}, o.card ≤ ↑n ↔ o ≤ ↑n
-- Mathlib.Data.List.Lex
List.lt_iff_lex_lt : ∀ {α : Type u} [inst : LT α] (l l' : List α), l.lt l' ↔ List.Lex (fun x1 x2 => x1 < x2) l l'
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.coe_pi : ∀ {η : Type u_7} {f : η → Type u_8} [inst : (i : η) → AddGroup (f i)] (I : Set η) (H : (i : η) → AddSubgroup (f i)),
  ↑(AddSubgroup.pi I H) = I.pi fun i => ↑(H i)
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- If `f` admits a Taylor series `p` in a set `s`, and `g` is affine, then `f ∘ g` admits a Taylor
series in `g ⁻¹' s`, whose `k`-th term at `x` is given
by `p (g x) k (g.contLinear v₁, ..., g.contLinear vₖ)` .  -/
HasFTaylorSeriesUpToOn.comp_continuousAffineMap : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {f : E → F} {n : WithTop ℕ∞}
  {p : E → FormalMultilinearSeries 𝕜 E F},
  HasFTaylorSeriesUpToOn n f p s →
    ∀ (g : G →ᴬ[𝕜] E),
      HasFTaylorSeriesUpToOn n (f ∘ ⇑g) (fun x k => (p (g x) k).compContinuousLinearMap fun x => g.contLinear)
        (⇑g ⁻¹' s)
-- Mathlib.Data.NNReal.Defs
NNReal.inv_lt_one_iff : ∀ {x : NNReal}, x ≠ 0 → (x⁻¹ < 1 ↔ 1 < x)
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.instNonUnitalNormedCommRing : {α : Type u_1} →
  [inst : TopologicalSpace α] →
    [CompactSpace α] → {R : Type u_4} → [inst_2 : NonUnitalNormedCommRing R] → NonUnitalNormedCommRing C(α, R)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
Orientation.rotation_eq_matrix_toLin : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle) {x : V} (hx : x ≠ 0),
  ↑(o.rotation θ).toLinearEquiv =
    (Matrix.toLin (o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx)) !![θ.cos, -θ.sin; θ.sin, θ.cos]
-- Mathlib.RingTheory.Ideal.Quotient.Nilpotent
IsNilpotent.isUnit_quotient_mk_iff : ∀ {R : Type u_2} [inst : CommRing R] {I : Ideal R},
  IsNilpotent I → ∀ {x : R}, IsUnit ((Ideal.Quotient.mk I) x) ↔ IsUnit x
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.lt_one_iff : ∀ {n : ℕ} (a : BitVec n), 0 < n → a.ult 1#n = (a == 0#n)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.add_eq_coe : ∀ {α : Type u} [inst : Add α] {a b : WithBot α} {c : α}, a + b = ↑c ↔ ∃ a' b', ↑a' = a ∧ ↑b' = b ∧ a' + b' = c
-- Init.Internal.Order.Lemmas
_private.Init.Internal.Order.Lemmas.0.Array.findSomeRevM?.find.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (r : Option β) → ((val : β) → motive (some val)) → (Unit → motive none) → motive r
-- Init.Grind.Ring.CommSemiringAdapter
_private.Init.Grind.Ring.CommSemiringAdapter.0.Lean.Grind.CommRing.Expr.toPolyS.match_4.eq_8 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (a : Lean.Grind.CommRing.Expr)
  (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_3 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_4 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b))
  (h_5 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k))
  (h_6 : (n : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast n))
  (h_7 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b)) (h_8 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_9 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k)),
  (match a.neg with
    | Lean.Grind.CommRing.Expr.num n => h_1 n
    | Lean.Grind.CommRing.Expr.var x => h_2 x
    | a.add b => h_3 a b
    | a.mul b => h_4 a b
    | a.pow k => h_5 a k
    | Lean.Grind.CommRing.Expr.natCast n => h_6 n
    | a.sub b => h_7 a b
    | a.neg => h_8 a
    | Lean.Grind.CommRing.Expr.intCast k => h_9 k) =
    h_8 a
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.exists_isBasis_subset_isBasis : ∀ {α : Type u_1} {X Y : Set α} (M : Matroid α),
  X ⊆ Y →
    autoParam (Y ⊆ M.E) Matroid.exists_isBasis_subset_isBasis._auto_1 → ∃ I J, M.IsBasis I X ∧ M.IsBasis J Y ∧ I ⊆ J
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.instSuccOrder : SuccOrder Ordinal.{u}
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Comonad.ForgetCreatesColimits'.liftedCocone_ι_app_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {T : CategoryTheory.Comonad C} (D : CategoryTheory.Functor J T.Coalgebra)
  (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c) (j : J),
  ((CategoryTheory.Comonad.ForgetCreatesColimits'.liftedCocone D c t).ι.app j).f = c.ι.app j
-- Init.Core
Except.ok.inj : ∀ {ε : Type u} {α : Type v} {a a_1 : α}, Except.ok a = Except.ok a_1 → a = a_1
-- Mathlib.Analysis.InnerProductSpace.Rayleigh
IsSelfAdjoint.linearly_dependent_of_isLocalExtrOn : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] [inst_2 : CompleteSpace F]
  {T : F →L[ℝ] F},
  IsSelfAdjoint T →
    ∀ {x₀ : F}, IsLocalExtrOn T.reApplyInnerSelf (Metric.sphere 0 ‖x₀‖) x₀ → ∃ a b, (a, b) ≠ 0 ∧ a • x₀ + b • T x₀ = 0
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.leftInverse_trunc_toLaurent : ∀ {R : Type u_1} [inst : Semiring R], Function.LeftInverse ⇑LaurentPolynomial.trunc ⇑Polynomial.toLaurent
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.compIso_inv_comp_image_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasEqualizers C] [inst_2 : CategoryTheory.Limits.HasImage f]
  [inst_3 : CategoryTheory.IsIso g] {Z_1 : C} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.compIso f g).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv g) h)
-- Init.Data.Int.Order
Int.le_of_lt : ∀ {a b : ℤ}, a < b → a ≤ b
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.instCountablyGeneratedSubtype : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSpace.CountablyGenerated α] {p : α → Prop},
  MeasurableSpace.CountablyGenerated { x // p x }
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_insert : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α} {v : β k}, a ∈ m.insert k v ↔ (k == a) = true ∨ a ∈ m
-- Mathlib.Data.Finmap
Finmap.induction_on : ∀ {α : Type u} {β : α → Type v} {C : Finmap β → Prop} (s : Finmap β), (∀ (a : AList β), C a.toFinmap) → C s
-- Mathlib.Algebra.Lie.OfAssociative
LieSubmodule.toEnd_comp_subtype_mem : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (N : LieSubmodule R L M) (x : L) (m : M) (hm : m ∈ ↑N), ((LieModule.toEnd R L M) x ∘ₗ (↑N).subtype) ⟨m, hm⟩ ∈ ↑N
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
/-- The empty space is initial in `LocallyRingedSpace`.  -/
AlgebraicGeometry.LocallyRingedSpace.emptyIsInitial : CategoryTheory.Limits.IsInitial ∅
-- Mathlib.RepresentationTheory.Basic
Representation.IsTrivial.out : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} {inst : Semiring k} {inst_1 : Monoid G} {inst_2 : AddCommMonoid V}
  {inst_3 : Module k V} {ρ : Representation k G V} [self : ρ.IsTrivial] (g : G), ρ g = LinearMap.id
-- Mathlib.CategoryTheory.Functor.Category
/-- Flip the arguments of a bifunctor. See also `Currying.lean`.  -/
CategoryTheory.Functor.flip : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            CategoryTheory.Functor C (CategoryTheory.Functor D E) →
              CategoryTheory.Functor D (CategoryTheory.Functor C E)
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the smallest key that is greater than or equal to the
given key, returning `none` if no such key exists.
 -/
Std.DTreeMap.Raw.getKeyGE? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → α → Option α
-- Lean.CoreM
Lean.Core.SavedState.mk.inj : ∀ {toState : Lean.Core.State} {passedHeartbeats : ℕ} {toState_1 : Lean.Core.State} {passedHeartbeats_1 : ℕ},
  { toState := toState, passedHeartbeats := passedHeartbeats } =
      { toState := toState_1, passedHeartbeats := passedHeartbeats_1 } →
    toState = toState_1 ∧ passedHeartbeats = passedHeartbeats_1
-- Mathlib.Algebra.Group.Subgroup.Ker
/-- The subgroup of elements `x : G` such that `f x = g x`  -/
MonoidHom.eqLocus : {G : Type u_1} → [inst : Group G] → {M : Type u_7} → [inst_1 : Monoid M] → (G →* M) → (G →* M) → Subgroup G
-- Mathlib.Data.Ordmap.Ordset
_private.Mathlib.Data.Ordmap.Ordset.0.Ordnode.size.match_1.eq_1 : ∀ {α : Type u_1} (motive : Ordnode α → Sort u_2) (h_1 : Unit → motive Ordnode.nil)
  (h_2 : (sz : ℕ) → (l : Ordnode α) → (x : α) → (r : Ordnode α) → motive (Ordnode.node sz l x r)),
  (match Ordnode.nil with
    | Ordnode.nil => h_1 ()
    | Ordnode.node sz l x r => h_2 sz l x r) =
    h_1 ()
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
/-- Converts a Lie-Rinehart subalgebra to the corresponding Lie subalgebra.  -/
LieRinehartSubalgebra.toLieSubalgebra : {A : Type u_1} →
  {L : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : LieRing L] →
        [inst_2 : Module A L] →
          LieRinehartSubalgebra 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] → [LieRinehartAlgebra R A L] → LieSubalgebra R L
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.Ico_add_one_add_one_eq_Ioc_of_not_isMax : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Add α]
  [SuccAddOrder α] {b : α}, ¬IsMax b → ∀ (a : α), Finset.Ico (a + 1) (b + 1) = Finset.Ioc a b
-- Mathlib.Topology.Bases
IsTopologicalBasis.iInf_induced : ∀ {β : Type u_1} {ι : Type u_2} {X : ι → Type u_3} [t : (i : ι) → TopologicalSpace (X i)]
  {T : (i : ι) → Set (Set (X i))},
  (∀ (i : ι), TopologicalSpace.IsTopologicalBasis (T i)) →
    ∀ (f : (i : ι) → β → X i),
      TopologicalSpace.IsTopologicalBasis {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i}
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, (m₁ ∩ m₂).contains k = (m₁.contains k && m₂.contains k)
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
IsAddKleinFour.exponent_two : ∀ {G : Type u_1} {inst : AddGroup G} [self : IsAddKleinFour G], AddMonoid.exponent G = 2
-- Mathlib.Combinatorics.Matroid.Map
Matroid.comap_isBase_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {N : Matroid β} {B : Set α},
  (N.comap f).IsBase B ↔ N.IsBasis (f '' B) (f '' f ⁻¹' N.E) ∧ Set.InjOn f B ∧ B ⊆ f ⁻¹' N.E
-- Mathlib.RingTheory.Ideal.Defs
Ideal.pow_mem_of_pow_mem : ∀ {α : Type u} [inst : Semiring α] (I : Ideal α) {a : α} {m n : ℕ}, a ^ m ∈ I → m ≤ n → a ^ n ∈ I
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
IsProperSemilinearSet.biUnion : ∀ {M : Type u_1} {ι : Type u_3} [inst : AddCommMonoid M] {s : Set ι} {t : ι → Set M},
  s.Finite → (∀ i ∈ s, IsProperSemilinearSet (t i)) → IsProperSemilinearSet (⋃ i ∈ s, t i)
-- Mathlib.MeasureTheory.Group.Arithmetic
Pi.measurableSub₂ : ∀ {ι : Type u_5} {α : ι → Type u_6} [inst : (i : ι) → Sub (α i)] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  [∀ (i : ι), MeasurableSub₂ (α i)], MeasurableSub₂ ((i : ι) → α i)
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.succ.sizeOf_spec : sizeOf Turing.ToPartrec.Code.succ = 1
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.erase.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M) (x : AddMonoidAlgebra R M),
  AddMonoidAlgebra.erase m x = AddMonoidAlgebra.ofCoeff (Finsupp.erase m x.coeff)
-- Lean.Meta.Check
_private.Lean.Meta.Check.0.Lean.Meta.addPPExplicitToExposeDiff.visit : Lean.Expr → Lean.Expr → Lean.MetaM (Lean.Expr × Lean.Expr)
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.PreOneHypercover.functorPushforward_sieve₁_map_le : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : C} {E : CategoryTheory.PreOneHypercover X} (F : CategoryTheory.Functor C D) {W : C} {i₁ i₂ : E.I₀}
  (p₁ : W ⟶ E.X i₁) (p₂ : W ⟶ E.X i₂),
  CategoryTheory.Sieve.functorPushforward F (E.sieve₁ p₁ p₂) ≤ (E.map F).sieve₁ (F.map p₁) (F.map p₂)
-- Init.Data.Vector.Find
Vector.getElem_zero_flatten.proof : ∀ {α : Type u_1} {m n : ℕ} {xss : Vector (Vector α m) n},
  0 < n * m → (Vector.findSome? (fun xs => xs[0]?) xss).isSome = true
-- Init.Omega.Constraint
Lean.Omega.tidy_sat : ∀ {s : Lean.Omega.Constraint} {x v : Lean.Omega.Coeffs},
  s.sat' x v = true → (Lean.Omega.tidyConstraint s x).sat' (Lean.Omega.tidyCoeffs s x) v = true
-- Init.Data.Int.Cooper
Int.Cooper.resolve_left_inv_dvd : ∀ {s : ℤ} (a c d p k : ℤ),
  0 < a → a ∣ k + p → a * d ∣ c * k + c * p + a * s → d ∣ c * Int.Cooper.resolve_left_inv a p k + s
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.SmallShiftedHom.mk₀Inv_comp_mk₀ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W : CategoryTheory.MorphismProperty C} {M : Type w'}
  [inst_1 : AddMonoid M] [inst_2 : CategoryTheory.HasShift C M] {X Y : C}
  [inst_3 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y]
  [inst_4 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X X]
  [inst_5 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y X] [inst_6 : W.IsCompatibleWithShift M]
  [inst_7 : W.RespectsIso] (m₀ : M) (hm₀ : m₀ = 0) (f : Y ⟶ X) (hf : W f),
  (CategoryTheory.Localization.SmallShiftedHom.mk₀Inv m₀ hm₀ f hf).comp
      (CategoryTheory.Localization.SmallShiftedHom.mk₀ W m₀ hm₀ f) ⋯ =
    CategoryTheory.Localization.SmallShiftedHom.mk₀ W m₀ hm₀ (CategoryTheory.CategoryStruct.id X)
-- Mathlib.Algebra.Order.Star.Basic
one_le_star_iff : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R] {x : R},
  1 ≤ star x ↔ 1 ≤ x
-- Mathlib.Order.SuccPred.Basic
/-- **Alias** of `Order.pred_le_of_wcovBy`.

---

See also `Order.pred_eq_of_covBy`.  -/
WCovBy.pred_le : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a b : α}, b ⩿ a → Order.pred a ≤ b
-- Mathlib.Algebra.Group.Action.Prod
MulAction.prodEquiv.eq_1 : ∀ (M : Type u_1) (N : Type u_2) (α : Type u_5) [inst : Monoid M] [inst_1 : Monoid N],
  MulAction.prodEquiv M N α =
    { toFun := fun x => ⟨MulAction.compHom α (MonoidHom.inl M N), ⟨MulAction.compHom α (MonoidHom.inr M N), ⋯⟩⟩,
      invFun := fun _insts =>
        have this := ⋯;
        MulAction.prodOfSMulCommClass M N α,
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.CategoryTheory.Localization.Trifunctor
CategoryTheory.Localization.Lifting₃.uncurry : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {D₁ : Type u_6} →
        {D₂ : Type u_7} →
          {D₃ : Type u_8} →
            {E : Type u_13} →
              [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
                [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
                  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
                    [inst_3 : CategoryTheory.Category.{v_4, u_6} D₁] →
                      [inst_4 : CategoryTheory.Category.{v_5, u_7} D₂] →
                        [inst_5 : CategoryTheory.Category.{v_6, u_8} D₃] →
                          [inst_6 : CategoryTheory.Category.{v_13, u_13} E] →
                            (L₁ : CategoryTheory.Functor C₁ D₁) →
                              (L₂ : CategoryTheory.Functor C₂ D₂) →
                                (L₃ : CategoryTheory.Functor C₃ D₃) →
                                  (W₁ : CategoryTheory.MorphismProperty C₁) →
                                    (W₂ : CategoryTheory.MorphismProperty C₂) →
                                      (W₃ : CategoryTheory.MorphismProperty C₃) →
                                        (F :
                                            CategoryTheory.Functor C₁
                                              (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) →
                                          (F' :
                                              CategoryTheory.Functor D₁
                                                (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) →
                                            [CategoryTheory.Localization.Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F F'] →
                                              CategoryTheory.Localization.Lifting (L₁.prod (L₂.prod L₃))
                                                (W₁.prod (W₂.prod W₃)) (CategoryTheory.Functor.uncurry₃.obj F)
                                                (CategoryTheory.Functor.uncurry₃.obj F')
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haarMeasure.congr_simp : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (K₀ K₀_1 : TopologicalSpace.PositiveCompacts G),
  K₀ = K₀_1 → MeasureTheory.Measure.haarMeasure K₀ = MeasureTheory.Measure.haarMeasure K₀_1
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_ofList_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l → (Std.ExtHashMap.ofList l).getKey? k' = some k
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_24 : HAdd Std.Time.Hour.Offset Std.Time.Nanosecond.Offset Std.Time.Nanosecond.Offset