mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Immersion
/-- A choice of complement of the model normed space `E` of `M` in the model normed space
`E'` of `N`  -/
Manifold.IsImmersion.complement : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      {E'' : Type u} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup E''] →
              [inst_4 : NormedSpace 𝕜 E''] →
                {H : Type u_7} →
                  [inst_5 : TopologicalSpace H] →
                    {G : Type u_9} →
                      [inst_6 : TopologicalSpace G] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {J : ModelWithCorners 𝕜 E'' G} →
                            {M : Type u_11} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H M] →
                                  {N : Type u_13} →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace G N] →
                                        {n : WithTop ℕ∞} → {f : M → N} → Manifold.IsImmersion I J n f → Type u
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.lt.sizeOf_spec : ∀ (lhs rhs : ℕ) (proof : Lean.Expr),
  sizeOf (Mathlib.Tactic.Order.AtomicFact.lt lhs rhs proof) = 1 + sizeOf lhs + sizeOf rhs + sizeOf proof
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_add_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIocDiv hp a (b + p) = toIocDiv hp a b + 1
-- Mathlib.Algebra.Module.Submodule.Range
/-- If `O` is a submodule of `M`, and `Φ : O →ₗ M'` is a linear map,
then `(ϕ : O →ₗ M').submoduleImage N` is `ϕ(N)` as a submodule of `M'`  -/
LinearMap.submoduleImage : {R : Type u_1} →
  {M : Type u_5} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {M' : Type u_10} →
            [inst_3 : AddCommMonoid M'] →
              [inst_4 : Module R M'] → {O : Submodule R M} → (↥O →ₗ[R] M') → Submodule R M → Submodule R M'
-- Init.Data.String.Defs
String.offset_endPos : ∀ {s : String}, s.endPos.offset = s.rawEndPos
-- Mathlib.Analysis.Convex.Intrinsic
intrinsicClosure_mono : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] {s t : Set P},
  s ⊆ t → intrinsicClosure 𝕜 s ⊆ intrinsicClosure 𝕜 t
-- Mathlib.Topology.EMetricSpace.Defs
ULift.edist_eq : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (x y : ULift.{u_2, u} α), edist x y = edist x.down y.down
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.toList_eq_match_rci : ∀ {α : Type u} {r : Std.Roi α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.Rxi.IsAlwaysFinite α],
  r.toList =
    match Std.PRange.succ? r.lower with
    | none => []
    | some next => next...*.toList
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
CategoryTheory.Functor.IsStronglyCocartesian.of_iso : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ≅ b) [p.IsHomLift f φ.hom],
  p.IsStronglyCocartesian f φ.hom
-- Mathlib.Algebra.Polynomial.RingDivision
Polynomial.modByMonicHom_apply : ∀ {R : Type u} [inst : CommRing R] (q p : Polynomial R), q.modByMonicHom p = p %ₘ q
-- Mathlib.Analysis.Normed.Group.HomCompletion
NormedAddCommGroup.norm_toCompl : ∀ {G : Type u_1} [inst : SeminormedAddCommGroup G] (x : G), ‖NormedAddCommGroup.toCompl x‖ = ‖x‖
-- Mathlib.LinearAlgebra.Basis.Prod
Module.Basis.prod_repr_inr : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M']
  (b : Module.Basis ι R M) (b' : Module.Basis ι' R M') (x : M × M') (i : ι'),
  ((b.prod b').repr x) (Sum.inr i) = (b'.repr x.2) i
-- Mathlib.Algebra.BigOperators.Group.List.Basic
AddMonoidHom.map_list_sum : ∀ {M : Type u_4} {N : Type u_5} [inst : AddMonoid M] [inst_1 : AddMonoid N] (f : M →+ N) (l : List M),
  f l.sum = (List.map (⇑f) l).sum
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.instLinearOrderedAddCommMonoidWithTop : {α : Type u_2} → [LinearOrderedAddCommGroupWithTop α] → LinearOrderedAddCommMonoidWithTop α
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.equivQuotientZPowOfEquiv.eq_1 : ∀ {A B : Type u} [inst : CommGroup A] [inst_1 : CommGroup B] (e : A ≃* B) (n : ℤ),
  QuotientGroup.equivQuotientZPowOfEquiv e n =
    (QuotientGroup.homQuotientZPowOfHom (↑e) n).toMulEquiv (QuotientGroup.homQuotientZPowOfHom (↑e.symm) n) ⋯ ⋯
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_15.eq_5 : ∀ (motive : Std.Tactic.BVDecide.BVUnOp → Sort u_1) (h_1 : Unit → motive Std.Tactic.BVDecide.BVUnOp.not)
  (h_2 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateLeft distance))
  (h_3 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateRight distance))
  (h_4 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst distance))
  (h_5 : Unit → motive Std.Tactic.BVDecide.BVUnOp.reverse) (h_6 : Unit → motive Std.Tactic.BVDecide.BVUnOp.clz)
  (h_7 : Unit → motive Std.Tactic.BVDecide.BVUnOp.cpop),
  (match Std.Tactic.BVDecide.BVUnOp.reverse with
    | Std.Tactic.BVDecide.BVUnOp.not => h_1 ()
    | Std.Tactic.BVDecide.BVUnOp.rotateLeft distance => h_2 distance
    | Std.Tactic.BVDecide.BVUnOp.rotateRight distance => h_3 distance
    | Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst distance => h_4 distance
    | Std.Tactic.BVDecide.BVUnOp.reverse => h_5 ()
    | Std.Tactic.BVDecide.BVUnOp.clz => h_6 ()
    | Std.Tactic.BVDecide.BVUnOp.cpop => h_7 ()) =
    h_5 ()
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
/-- If `ζ - 1` does not divide `x`, then `p` and `x` are coprime, where `ζ` is a primitive `p`-th
root of unity and `p` is prime.  -/
IsCyclotomicExtension.Rat.isCoprime_of_not_zeta_sub_one_dvd : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  [hK : IsCyclotomicExtension {p} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ p) {x : NumberField.RingOfIntegers K},
  ¬hζ.toInteger - 1 ∣ x → IsCoprime (↑p) x
-- Mathlib.Topology.Connected.PathConnected
isPathConnected_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] (x : X), IsPathConnected {x}
-- Std.Async.System
Std.Async.System.SystemUser.mk.sizeOf_spec : ∀ (username : String) (userId : Option Std.Async.System.UserId) (groupId : Option Std.Async.System.GroupId)
  (shell : Option String) (homeDir : Option System.FilePath),
  sizeOf { username := username, userId := userId, groupId := groupId, shell := shell, homeDir := homeDir } =
    1 + sizeOf username + sizeOf userId + sizeOf groupId + sizeOf shell + sizeOf homeDir
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey!_insertEntry_le_self : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {v : β k}, (compare (Std.Internal.List.minKey! (Std.Internal.List.insertEntry k v l)) k).isLE = true
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_compl : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsFiniteMeasure μ],
  MeasurableSet s → μ.real sᶜ = μ.real Set.univ - μ.real s
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.map.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f f_1 : X ⟶ Y) (e_f : f = f_1)
  [inst_1 : CategoryTheory.Mono f], CategoryTheory.Subobject.map f = CategoryTheory.Subobject.map f_1
-- Mathlib.Order.BoundedOrder.Basic
not_isMin_iff_ne_bot : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, ¬IsMin a ↔ a ≠ ⊥
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_diff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, (t₁ \ t₂).contains k = (t₁.contains k && !t₂.contains k)
-- Mathlib.Algebra.CubicDiscriminant
Cubic.coeff_eq_a : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.toPoly.coeff 3 = P.a
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.hasLimit_of_domain_hasInitial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  [CategoryTheory.Limits.HasInitial J] {F : CategoryTheory.Functor J C}, CategoryTheory.Limits.HasLimit F
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.IsAffineOpen.fromSpecStalk_closedPoint : ∀ {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↥X} (hU : AlgebraicGeometry.IsAffineOpen U) {x : ↥X}
  (hxU : x ∈ U), (hU.fromSpecStalk hxU) (IsLocalRing.closedPoint ↑(X.presheaf.stalk x)) = x
-- Mathlib.RingTheory.AlgebraTower
/-- `Basis.smulTower (b : Basis ι R S) (c : Basis ι S A)` is the `R`-basis on `A`
where the `(i, j)`th basis vector is `b i • c j`.  -/
Module.Basis.smulTower : {R : Type u_1} →
  {S : Type u_2} →
    {A : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : Semiring S] →
          [inst_2 : AddCommMonoid A] →
            [inst_3 : Module R S] →
              [inst_4 : Module S A] →
                [inst_5 : Module R A] →
                  [IsScalarTower R S A] →
                    {ι : Type u_5} →
                      {ι' : Type u_6} → Module.Basis ι R S → Module.Basis ι' S A → Module.Basis (ι × ι') R A
-- Lean.SubExpr
Lean.SubExpr.GoalsLocation.loc : Lean.SubExpr.GoalsLocation → Lean.SubExpr.GoalLocation
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.pushforwardIsoBind_inv_h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (E : CategoryTheory.PreZeroHypercover X)
  (i : ((CategoryTheory.PreZeroHypercover.singleton f).bind fun x => E).I₀),
  (CategoryTheory.PreZeroHypercover.pushforwardIsoBind f E).inv.h₀ i = CategoryTheory.CategoryStruct.id (E.X i.snd)
-- Init.Data.UInt.Lemmas
UInt8.toUSize_ofNat : ∀ {n : ℕ}, n < 256 → (OfNat.ofNat n).toUSize = OfNat.ofNat n
-- Mathlib.RingTheory.MvPolynomial.Groebner
MonomialOrder.subLTerm.eq_1 : ∀ {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [inst : CommRing R] (f : MvPolynomial σ R),
  m.subLTerm f = f - (MvPolynomial.monomial (m.degree f)) (m.leadingCoeff f)
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.uniqueDiffOn_image_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  (e : E ≃L[𝕜] F), UniqueDiffOn 𝕜 (⇑e '' s) ↔ UniqueDiffOn 𝕜 s
-- Mathlib.Order.Atoms
IsAtom.not_le_iff_disjoint : ∀ {α : Type u_2} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b : α}, IsAtom a → (¬a ≤ b ↔ Disjoint a b)
-- Mathlib.Data.QPF.Univariate.Basic
QPF.Fix.rec_eq : ∀ {F : Type u → Type u} [q : QPF F] {α : Type u} (g : F α → α) (x : F (QPF.Fix F)),
  QPF.Fix.rec g (QPF.Fix.mk x) = g (QPF.Fix.rec g <$> x)
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.padic_norm_e_of_padicInt : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (z : ℤ_[p]), ‖↑z‖ = ‖z‖
-- Mathlib.Algebra.Ring.Parity
Odd.add_odd : ∀ {α : Type u_2} [inst : Semiring α] {a b : α}, Odd a → Odd b → Even (a + b)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Fintype.prod_eq_one_iff_of_le_one : ∀ {ι : Type u_9} {M : Type u_10} [inst : Fintype ι] [inst_1 : CommMonoid M] [inst_2 : PartialOrder M] [MulLeftMono M]
  {f : ι → M}, f ≤ 1 → (∏ i, f i = 1 ↔ f = 1)
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- **Alias** of the reverse direction of `differentiableOn_const_add_iff`. -/
DifferentiableOn.const_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {s : Set E} (c : F), DifferentiableOn 𝕜 f s → DifferentiableOn 𝕜 (fun y => c + f y) s
-- Mathlib.Algebra.Order.Module.Defs
Pi.instPosSMulMono : ∀ {α : Type u_1} {ι : Type u_3} {β : ι → Type u_4} [inst : Zero α] [inst_1 : Preorder α]
  [inst_2 : (i : ι) → Preorder (β i)] [inst_3 : (i : ι) → SMul α (β i)] [∀ (i : ι), PosSMulMono α (β i)],
  PosSMulMono α ((i : ι) → β i)
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.uniqueBaseOn_empty : ∀ {α : Type u_1} (I : Set α), Matroid.uniqueBaseOn ∅ I = Matroid.loopyOn I
-- Mathlib.CategoryTheory.ObjectProperty.InheritedFromHom
CategoryTheory.ObjectProperty.InheritedFromTarget.of_le : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  (Q Q' : CategoryTheory.MorphismProperty C), Q ≤ Q' → ∀ [P.InheritedFromTarget Q'], P.InheritedFromTarget Q
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.UnsatProof.le.inj : ∀ {c c_1 : Lean.Meta.Grind.Arith.Cutsat.LeCnstr},
  Lean.Meta.Grind.Arith.Cutsat.UnsatProof.le c = Lean.Meta.Grind.Arith.Cutsat.UnsatProof.le c_1 → c = c_1
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Prequotient.one.sizeOf_spec : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} [inst_1 : SizeOf J],
  sizeOf RingCat.Colimits.Prequotient.one = 1
-- Mathlib.Topology.Bornology.Absorbs
absorbent_iff_forall_absorbs_singleton : ∀ {M : Type u_1} {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] {s : Set α},
  Absorbent M s ↔ ∀ (x : α), Absorbs M s {x}
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
MeasureTheory.enorm_indicatorConstLp_le : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E},
  ‖MeasureTheory.indicatorConstLp p hs hμs c‖ₑ ≤ ‖c‖ₑ * μ s ^ (1 / p.toReal)
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.instFinitenessRelation : {α : Type u_1} → {β : Type u_2} → Std.Iterators.FinitenessRelation (Lean.PersistentHashMap.Zipper α β) Id
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.instMonoidalCategory : CategoryTheory.MonoidalCategory SFinKer
-- Init.Data.Vector.Lemmas
Vector.getElem_toList : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} (h : i < xs.toList.length), xs.toList[i] = xs[i]
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get_union_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α] (h₁ : (↑m₁).WF) (h₂ : (↑m₂).WF) {k : α} (contains_eq_false : m₂.contains k = false)
  {h' : (m₁.union m₂).contains k = true}, (m₁.union m₂).get k h' = m₁.get k ⋯
-- Init.Data.List.Basic
/-- Returns the first element in the list, if there is one. Returns `none` if the list is empty.

Use `List.headD` to provide a fallback value for empty lists, or `List.head!` to panic on empty
lists.

Examples:
 * `([] : List Nat).head? = none`
 * `[3, 2, 1].head? = some 3`
 -/
List.head? : {α : Type u} → List α → Option α
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.sinh_half_dist_add_dist : ∀ (a b c : UpperHalfPlane),
  Real.sinh ((dist a b + dist b c) / 2) =
    (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist ↑b ↑c * dist (↑a) ((starRingEnd ℂ) ↑b)) /
      (2 * √(a.im * c.im) * dist (↑b) ((starRingEnd ℂ) ↑b))
-- Mathlib.Data.Sym.Sym2
Equiv.sigmaFiberFromRel_apply : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} (sym : Std.Symm r) {f : α → β} (hf : r ≤ ⇑(Setoid.ker f))
  (z : ↑(Sym2.fromRel sym)),
  (Equiv.sigmaFiberFromRel sym hf) z = Sym2.fromRelNdrec ↑z ⋯ (fun a₁ a₂ h => ⟨f a₁, ⟨s(⟨a₁, ⋯⟩, ⟨a₂, ⋯⟩), h⟩⟩) ⋯
-- Mathlib.RingTheory.LocalRing.LocalSubring
LocalSubring.ext_iff : ∀ {R : Type u_1} {inst : CommRing R} {x y : LocalSubring R}, x = y ↔ x.toSubring = y.toSubring
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.State.failed.injEq : ∀ {dir : Std.Http.Protocol.H1.Direction} (error error_1 : Std.Http.Protocol.H1.Error),
  (Std.Http.Protocol.H1.Reader.State.failed error = Std.Http.Protocol.H1.Reader.State.failed error_1) =
    (error = error_1)
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.fromEdgeSet_le : ∀ {V : Type u} (G : SimpleGraph V) {s : Set (Sym2 V)}, SimpleGraph.fromEdgeSet s ≤ G ↔ s \ Sym2.diagSet ⊆ G.edgeSet
-- Std.Data.HashSet.Lemmas
Std.HashSet.isEmpty_eq_false_iff_exists_contains_eq_true : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  m.isEmpty = false ↔ ∃ a, m.contains a = true
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.IsOrtho.inner_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U V : Submodule 𝕜 E}, U ⟂ V → ∀ {u v : E}, u ∈ U → v ∈ V → inner 𝕜 u v = 0
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_minKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = false → t.getKey? t.minKey! = some t.minKey!
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.restrict_isStrictRestriction : ∀ {α : Type u_1} {R : Set α} {M : Matroid α}, R ⊂ M.E → (M.restrict R).IsStrictRestriction M
-- Std.Time.Time.HourMarker
Std.Time.instReprHourMarker : Repr Std.Time.HourMarker
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.NatTrans.prod_app_fst : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] {F G : CategoryTheory.Functor A B} {H I : CategoryTheory.Functor C D}
  (α : F ⟶ G) (β : H ⟶ I) (X : A × C), ((CategoryTheory.NatTrans.prod α β).app X).1 = α.app X.1
-- Init.Data.String.Lemmas.FindPos
String.Slice.offset_posLE_eq_self_iff : ∀ {s : String.Slice} {p : String.Pos.Raw}, (s.posLE p).offset = p ↔ String.Pos.Raw.IsValidForSlice s p
-- Mathlib.CategoryTheory.Limits.Presheaf
/-- If `F : C ⥤ Type w` and `C` is locally `w`-small, then for any `X : C`,
this is the colimit cocone which identifies `F.obj X` to the colimit of
`(CategoryOfElements.π F).op ⋙ shrinkYoneda.obj X`.  -/
CategoryTheory.Functor.Elements.coconeπOpCompShrinkYonedaObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C] →
      (F : CategoryTheory.Functor C (Type w)) →
        (X : C) →
          CategoryTheory.Limits.Cocone
            ((CategoryTheory.CategoryOfElements.π F).op.comp (CategoryTheory.shrinkYoneda.{w, v₁, u₁}.obj X))
-- Mathlib.RepresentationTheory.Subrepresentation
Subrepresentation.submoduleSubrepresentationOrderIso_apply : ∀ {A : Type u_1} {G : Type u_2} {M : Type u_4} [inst : CommSemiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid M]
  [inst_3 : Module (MonoidAlgebra A G) M] (N : Submodule (MonoidAlgebra A G) M),
  Subrepresentation.submoduleSubrepresentationOrderIso N = Subrepresentation.ofSubmodule N
-- Mathlib.Data.Rel
SetRel.isSymm_univ : ∀ {α : Type u_1}, SetRel.IsSymm Set.univ
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
/-- A local diffeomorphism is a local homeomorphism.  -/
IsLocalDiffeomorph.isLocalHomeomorph : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} {f : M → N},
  IsLocalDiffeomorph I J n f → IsLocalHomeomorph f
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.lim.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (c : Urysohns.CU P) (x : X),
  c.lim x = ⨆ n, Urysohns.CU.approx n c x
-- Mathlib.MeasureTheory.Integral.DivergenceTheorem
_private.Mathlib.MeasureTheory.Integral.DivergenceTheorem.0.MeasureTheory.termBackFace_ : Lean.ParserDescr
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.mul_const' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_8} [inst : NormedRing 𝕜] {f : α → 𝕜},
  MeasureTheory.Integrable f μ → ∀ (c : 𝕜), MeasureTheory.Integrable (f * fun x => c) μ
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_top : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  [RingHomClass F R S], Ideal.map f ⊤ = ⊤
-- Init.Data.UInt.Lemmas
BitVec.ofNatLT_uInt32ToNat : ∀ (n : UInt32), n.toNat#'⋯ = n.toBitVec
-- Mathlib.Combinatorics.Matroid.Loop
/-- **Alias** of `Matroid.sdiff_indep_iff_indep_of_subset_coloops`. -/
Matroid.diff_indep_iff_indep_of_subset_coloops : ∀ {α : Type u_1} {M : Matroid α} {I K : Set α}, K ⊆ M.coloops → (M.Indep (I \ K) ↔ M.Indep I)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKeyD_insert_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  t.isEmpty = true → ∀ {fallback : α}, (t.insert k v).minKeyD fallback = k
-- Mathlib.CategoryTheory.Category.Basic
/-- Composition in a category is associative.  -/
CategoryTheory.Category.assoc : ∀ {obj : Type u} [self : CategoryTheory.Category.{v, u} obj] {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.Pos.skipWhile.eq_def : ∀ {ρ : Type} {s : String.Slice} (pos : s.Pos) (pat : ρ) [inst : String.Slice.Pattern.ForwardPattern pat],
  pos.skipWhile pat =
    match pos.skip? pat with
    | some nextCurr => if pos < nextCurr then nextCurr.skipWhile pat else pos
    | none => pos
-- Mathlib.Analysis.Convex.Segment
segment_inter_subset_endpoint_of_linearIndependent_sub : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [AddRightMono 𝕜] [inst_3 : AddCommGroup E]
  [inst_4 : Module 𝕜 E] {c x y : E}, LinearIndependent 𝕜 ![x - c, y - c] → segment 𝕜 c x ∩ segment 𝕜 c y ⊆ {c}
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.mk_cancel_common_right : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s s' : ↥S) (m : M), LocalizedModule.mk (s' • m) (s * s') = LocalizedModule.mk m s
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
/-- Constructor for short complexes in `ModuleCat.{v} R` taking as inputs
linear maps `f` and `g` and the vanishing of their composition.  -/
CategoryTheory.ShortComplex.moduleCatMk : {R : Type u} →
  [inst : Ring R] →
    {X₁ X₂ X₃ : Type v} →
      [inst_1 : AddCommGroup X₁] →
        [inst_2 : AddCommGroup X₂] →
          [inst_3 : AddCommGroup X₃] →
            [inst_4 : Module R X₁] →
              [inst_5 : Module R X₂] →
                [inst_6 : Module R X₃] →
                  (f : X₁ →ₗ[R] X₂) → (g : X₂ →ₗ[R] X₃) → g ∘ₗ f = 0 → CategoryTheory.ShortComplex (ModuleCat R)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.le_pullbacks : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C), P ≤ P.pullbacks
-- Init.Data.String.Lemmas.Pattern.Char
_private.Init.Data.String.Lemmas.Pattern.Char.0.String.Slice.revAll.eq_1 : ∀ {ρ : Type} (s : String.Slice) (pat : ρ) [inst : String.Slice.Pattern.BackwardPattern pat],
  s.revAll pat = (s.skipSuffixWhile pat == s.startPos)