mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- We say that a set `H : Set (X → α)` of functions is equicontinuous on a subset if the family
`(↑) : ↥H → (X → α)` is equicontinuous on that subset.  -/
Set.EquicontinuousOn : {X : Type u_3} → {α : Type u_6} → [tX : TopologicalSpace X] → [uα : UniformSpace α] → Set (X → α) → Set X → Prop
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.mul_const : ∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace M] [inst_1 : Mul M] {m : MeasurableSpace α} {f : α → M}
  [MeasurableMul M], Measurable f → ∀ (c : M), Measurable fun x => f x * c
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.Approx.CofixA.continue : {F : PFunctor.{uA, uB}} → PFunctor.Approx.CofixA F 0
-- Mathlib.Analysis.Normed.Module.Basic
instNonUnitalSeminormedRingRestrictScalars : {𝕜 : Type u_1} →
  {𝕜' : Type u_2} → {E : Type u_3} → [I : NonUnitalSeminormedRing E] → NonUnitalSeminormedRing (RestrictScalars 𝕜 𝕜' E)
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.notMem_bot : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M] {x : M}, x ∉ ⊥
-- Mathlib.Algebra.QuadraticDiscriminant
discrim.eq_1 : ∀ {R : Type u_1} [inst : Ring R] (a b c : R), discrim a b c = b ^ 2 - 4 * a * c
-- Mathlib.Algebra.Homology.HomologySequenceLemmas
CategoryTheory.ShortComplex.ShortExact.acyclic_X₂ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)},
  S.ShortExact → S.X₁.Acyclic → S.X₃.Acyclic → S.X₂.Acyclic
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.mem_comap : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] [inst_5 : AddCommMonoid F] [inst_6 : Module R F] {f : E →ₗ[R] F}
  {C : PointedCone R F} {x : E}, x ∈ PointedCone.comap f C ↔ f x ∈ C
-- Lean.Meta.Tactic.Repeat
_private.Lean.Meta.Tactic.Repeat.0.Lean.Meta.repeat'Core.go.eq_def : ∀ {m : Type → Type} {ε : Type u_1} {s : Type} [inst : Monad m] [inst_1 : MonadExcept ε m]
  [inst_2 : Lean.MonadBacktrack s m] [inst_3 : Lean.MonadMCtx m] (f : Lean.MVarId → m (List Lean.MVarId)) (a : ℕ)
  (a_1 : Bool) (a_2 : List Lean.MVarId) (a_3 : List (List Lean.MVarId)) (a_4 : Array Lean.MVarId),
  Lean.Meta.repeat'Core.go✝ f a a_1 a_2 a_3 a_4 =
    match a, a_1, a_2, a_3, a_4 with
    | x, p, [], [], acc => pure (p, acc)
    | n, p, [], goals :: stk, acc => Lean.Meta.repeat'Core.go✝ f n p goals stk acc
    | n, p, g :: goals, stk, acc => do
      let __do_lift ← g.isAssigned
      if __do_lift = true then Lean.Meta.repeat'Core.go✝ f n p goals stk acc
        else
          match n with
          | 0 => pure (p, List.foldl Array.appendList (acc.push g ++ goals) stk)
          | n.succ => do
            let __do_lift ← Lean.observing? (f g)
            match __do_lift with
              | some goals' => Lean.Meta.repeat'Core.go✝ f n true goals' (goals :: stk) acc
              | none => Lean.Meta.repeat'Core.go✝ f n p goals stk (acc.push g)
-- Std.Data.HashMap.Lemmas
Std.HashMap.get_getElem? : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α} {h : m[a]?.isSome = true}, m[a]?.get h = m[a]
-- Mathlib.Analysis.InnerProductSpace.Basic
real_inner_self_pos : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x : F}, 0 < inner ℝ x x ↔ x ≠ 0
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.sc₁_X₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.sc₁._auto_1),
  (X.sc₁ f g fg h n₀ n₁ hn₁).X₃ = (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ fg)
-- Mathlib.Data.Real.Pointwise
Real.mul_iSup_of_nonpos : ∀ {ι : Sort u_1} {r : ℝ}, r ≤ 0 → ∀ (f : ι → ℝ), r * ⨆ i, f i = ⨅ i, r * f i
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.σ.eq_1 : ∀ (g : GL (Fin 2) ℝ),
  UpperHalfPlane.σ g = if 0 < ↑(Matrix.GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE
-- Mathlib.Condensed.Discrete.Basic
/-- The discrete condensed object associated to an object of `C` is the constant sheaf at that object.
 -/
Condensed.discrete : (C : Type w) →
  [inst : CategoryTheory.Category.{u + 1, w} C] →
    [CategoryTheory.HasWeakSheafify (CategoryTheory.coherentTopology CompHaus) C] →
      CategoryTheory.Functor C (Condensed C)
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.instGMulIntOfHasDetPlusMinusOneFinOfNatNatReal : (Γ : Subgroup (GL (Fin 2) ℝ)) → [Γ.HasDetPlusMinusOne] → GradedMonoid.GMul (ModularForm Γ)
-- Mathlib.LinearAlgebra.Projection
Submodule.projectionOnto_apply_right : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (h : IsCompl p q) (x : ↥q), (p.projectionOnto q h) ↑x = 0
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.resLE.eq_1 : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) (U : Y.Opens) (V : X.Opens)
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
  f.resLE U V e = CategoryTheory.CategoryStruct.comp (X.homOfLE e) (f ∣_ U)
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
CategoryTheory.LaxFunctor.mapComp_assoc_left_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a b c d : B}
  (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)),
  CategoryTheory.CategoryStruct.comp ((F.map h).toFunctor.map ((F.mapComp f g).toNatTrans.app X))
      ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).toNatTrans.app X) =
    CategoryTheory.CategoryStruct.comp ((F.mapComp g h).toNatTrans.app ((F.map f).toFunctor.obj X))
      (CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).toNatTrans.app X)
        ((F.map₂ (CategoryTheory.Bicategory.associator f g h).inv).toNatTrans.app X))
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.BundledIterM.Equiv.eq_1 : ∀ (m : Type w → Type w') (β : Type w) [inst : Monad m] [inst_1 : LawfulMonad m] (ita itb : Std.BundledIterM m β),
  Std.BundledIterM.Equiv m β ita itb =
    (Std.Iterators.HetT.map (Std.IterStep.mapIterator (Quot.mk (Std.BundledIterM.Equiv m β))) ita.step =
      Std.Iterators.HetT.map (Std.IterStep.mapIterator (Quot.mk (Std.BundledIterM.Equiv m β))) itb.step)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
/-- If `η` is an oplax transformation between `F` and `G`, we have a 1-morphism
`η.app a : F.obj a ⟶ G.obj a` for each object `a : B`. We also have a 2-morphism
`η.naturality f : F.map f ≫ app b ⟶ app a ≫ G.map f` for each 1-morphism `f : a ⟶ b`.
These 2-morphisms satisfy the naturality condition, and preserve the identities and
the compositions modulo some adjustments of domains and codomains of 2-morphisms.
 -/
CategoryTheory.Oplax.OplaxTrans : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        CategoryTheory.OplaxFunctor B C → CategoryTheory.OplaxFunctor B C → Type (max (max (max u₁ v₁) v₂) w₂)
-- Mathlib.Analysis.Calculus.ContDiff.Deriv
ContDiffOn.continuousOn_deriv_of_isOpen : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f : 𝕜 → F} {s : Set 𝕜},
  ContDiffOn 𝕜 n f s → IsOpen s → 1 ≤ n → ContinuousOn (deriv f) s
-- Init.Data.Array.MapIdx
_private.Init.Data.Array.MapIdx.0.Array.mapFinIdxM.map.match_1.splitter : {α : Type u_1} →
  (as : Array α) →
    (j : ℕ) →
      (motive : (i : ℕ) → i + j = as.size → Sort u_2) →
        (i : ℕ) →
          (inv : i + j = as.size) →
            ((x : 0 + j = as.size) → motive 0 x) →
              ((i : ℕ) → (inv : i + 1 + j = as.size) → motive i.succ inv) → motive i inv
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.mem_vsub : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {s t : Set β} {a : α}, a ∈ s -ᵥ t ↔ ∃ x ∈ s, ∃ y ∈ t, x -ᵥ y = a
-- Mathlib.Data.Bool.Basic
Bool.decide_false_iff : ∀ (p : Prop) {x : Decidable p}, decide p = false ↔ ¬p
-- Std.Sync.Semaphore
_private.Std.Sync.Semaphore.0.Std.Semaphore.mk : Std.Mutex Std.SemaphoreState✝ → Std.Semaphore
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k a fallback : α},
      (t.erase k).getKeyD a fallback = if cmp k a = Ordering.eq then fallback else t.getKeyD a fallback
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.rawCh.formatter : Char → optParam Bool false → Lean.PrettyPrinter.FormatterM Unit
-- Mathlib.Data.Analysis.Filter
Filter.Realizer.mk.inj : ∀ {α : Type u_1} {f : Filter α} {σ : Type u_5} {F : CFilter (Set α) σ} {eq : F.toFilter = f} {σ_1 : Type u_5}
  {F_1 : CFilter (Set α) σ_1} {eq_1 : F_1.toFilter = f},
  { σ := σ, F := F, eq := eq } = { σ := σ_1, F := F_1, eq := eq_1 } → σ = σ_1 ∧ F ≍ F_1
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.instInhabitedSigmaQuotedConstMkStr1NilLevelExProdNat : Inhabited ((e : Q(ℕ)) × Mathlib.Tactic.Ring.Common.ExProdNat e)
-- Mathlib.CategoryTheory.Sites.Pretopology
CategoryTheory.Pretopology.mem_toGrothendieck : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (K : CategoryTheory.Pretopology C) (X : C) (S : CategoryTheory.Sieve X),
  S ∈ K.toGrothendieck X ↔ ∃ R ∈ K.coverings X, R ≤ S.arrows
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionClientCapabilities.mk : Option Bool →
  Option Bool →
    Option Bool →
      Option Bool →
        Option Bool →
          Option Lean.Lsp.CodeActionLiteralSupport →
            Option Lean.Lsp.ResolveSupport → Lean.Lsp.CodeActionClientCapabilities
-- Init.Data.Array.Find
Array.find?_flatten : ∀ {α : Type u_1} {xss : Array (Array α)} {p : α → Bool}, Array.find? p xss.flatten = Array.findSome? (Array.find? p) xss
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofTermInfo.injEq : ∀ (i i_1 : Lean.Elab.TermInfo), (Lean.Elab.Info.ofTermInfo i = Lean.Elab.Info.ofTermInfo i_1) = (i = i_1)
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
/-- The standard presentation of the `R`-module `⋀[R]^n M`.  -/
exteriorPower.presentation : (R : Type u) →
  [inst : CommRing R] →
    (n : ℕ) → (M : Type u_1) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Module.Presentation R ↥(⋀[R]^n M)
-- Mathlib.Algebra.BigOperators.Finprod
/-- If `t` is a finite set of pairwise disjoint finite sets, then the sum of `f a` over
`a ∈ ⋃₀ t` is the sum over `s ∈ t` of the sums of `f a` over `a ∈ s`.  -/
finsum_mem_sUnion : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {t : Set (Set α)},
  t.PairwiseDisjoint id →
    t.Finite →
      (∀ x ∈ t, x.Finite) → ∑ᶠ (a : α) (_ : a ∈ ⋃₀ t), f a = ∑ᶠ (s : Set α) (_ : s ∈ t) (a : α) (_ : a ∈ s), f a
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
/-- [Stacks Tag 030F](https://stacks.math.columbia.edu/tag/030F) -/
IsTranscendenceBasis.cardinalMk_eq : ∀ {ι : Type u} {R : Type u_1} {A : Type w} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Nontrivial R] [NoZeroDivisors A] {ι' : Type u} {y : ι' → A},
  IsTranscendenceBasis R x → IsTranscendenceBasis R y → Cardinal.mk ι = Cardinal.mk ι'
-- Mathlib.NumberTheory.Rayleigh
/-- Let `r > 1` and `1/r + 1/s = 1`. Then `B_r` and `B'_s` are disjoint (i.e. no collision exists).
 -/
_private.Mathlib.NumberTheory.Rayleigh.0.Beatty.no_collision : ∀ {r s : ℝ}, r.HolderConjugate s → Disjoint {x | ∃ k, beattySeq r k = x} {x | ∃ k, beattySeq' s k = x}
-- Mathlib.Data.Multiset.Count
Multiset.countP_eq_card : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Multiset α}, Multiset.countP p s = s.card ↔ ∀ a ∈ s, p a
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.alter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α],
  m₁.WF → m₂.WF → ∀ (k : α) (f : Option (β k) → Option (β k)), m₁.Equiv m₂ → (m₁.alter k f).Equiv (m₂.alter k f)
-- Init.Data.Iterators.Basic
Std.IterM.ext : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} {x y : Std.IterM m β}, x.internalState = y.internalState → x = y
-- Init.Data.List.Nat.Basic
List.min?_eq_some_iff' : ∀ {a : ℕ} {xs : List ℕ}, xs.min? = some a ↔ a ∈ xs ∧ ∀ b ∈ xs, a ≤ b
-- Mathlib.Topology.Convenient.Category
/-- The inclusion functor `toTopCat : GeneratedByTopCat X ⥤ TopCat`
is fully faithful.  -/
GeneratedByTopCat.fullyFaithfulToTopCat : {ι : Type t} → (X : ι → Type u) → [inst : (i : ι) → TopologicalSpace (X i)] → GeneratedByTopCat.toTopCat.FullyFaithful
-- Mathlib.Tactic.NormNum.GCD
/-- Evaluate the `Nat.gcd` function.  -/
Mathlib.Meta.NormNum.evalNatGCD : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Kleisli.mk_of : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {T : CategoryTheory.Monad C} (c : CategoryTheory.Kleisli T),
  { of := c.of } = c
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.brecOn.go : {motive : Int.Internal.Linear.Poly → Sort u} →
  (t : Int.Internal.Linear.Poly) →
    ((t : Int.Internal.Linear.Poly) → Int.Internal.Linear.Poly.below t → motive t) →
      motive t ×' Int.Internal.Linear.Poly.below t
-- Mathlib.SetTheory.ZFC.Class
Class.eq_univ_iff_forall : ∀ {A : Class.{u}}, A = Class.univ ↔ ∀ (x : ZFSet.{u}), A x
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.exists_countable_dense_no_zero_top : ∃ s, s.Countable ∧ Dense s ∧ 0 ∉ s ∧ ⊤ ∉ s
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.mk_add_mk : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {m1 m2 : M} {s1 s2 : ↥S},
  LocalizedModule.mk m1 s1 + LocalizedModule.mk m2 s2 = LocalizedModule.mk (s2 • m1 + s1 • m2) (s1 * s2)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.lift_fst_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y Z X : C} {f : Y ⟶ X} {g : Z ⟶ X}
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g] {W : C} (a : W ⟶ Y) (b : W ⟶ Z)
  (h : autoParam (CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g) _auto_80✝) {Z_1 : C}
  (h_1 : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.lift a b h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.fst f g) h_1) =
    CategoryTheory.CategoryStruct.comp a h_1
-- Init.Data.UInt.Lemmas
UInt16.toBitVec_mul : ∀ {a b : UInt16}, (a * b).toBitVec = a.toBitVec * b.toBitVec
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.instUniformSpace : (K : Type u_2) → [inst : Field K] → UniformSpace (LaurentSeries K)
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.setInterior_mono : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {I J : Set k},
  I ⊆ J → ∀ {n : ℕ} (s : Affine.Simplex k P n), Affine.Simplex.setInterior I s ⊆ Affine.Simplex.setInterior J s
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
/-- **Alias** of `linearIndepOn_univ_iff`. -/
linearIndepOn_univ : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M], LinearIndepOn R v Set.univ ↔ LinearIndependent R v
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.map_φK : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂}
  {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (ψ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : h₁.IsPreservedBy F]
  [inst_6 : h₂.IsPreservedBy F], (ψ.map F).φK = F.map ψ.φK
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.SimprocDecl.keys : Lean.Meta.Simp.SimprocDecl → Array Lean.Meta.SimpTheoremKey
-- Init.Data.BitVec.Lemmas
BitVec.or_cast : ∀ {w w' : ℕ} {x y : BitVec w} (h : w = w'), BitVec.cast h x ||| BitVec.cast h y = BitVec.cast h (x ||| y)
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.uniqueBaseOn_indep_iff : ∀ {α : Type u_1} {E I J : Set α}, I ⊆ E → ((Matroid.uniqueBaseOn I E).Indep J ↔ J ⊆ I)
-- Batteries.Data.List.Lemmas
List.swap_swap : ∀ {α : Type u_1} {xs : List α} {i j : ℕ}, (xs.swap i j).swap i j = xs
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get?_erase_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, (m.erase k).get? k = none
-- Mathlib.CategoryTheory.Limits.Cones
/-- A cocone morphism between two cocones for the same diagram is a morphism of the cocone points
which commutes with the cocone legs.  -/
CategoryTheory.Limits.CoconeMorphism : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} → CategoryTheory.Limits.Cocone F → CategoryTheory.Limits.Cocone F → Type v₃
-- Init.Data.BitVec.Lemmas
/-- If two bitvectors have the same `msb`, then signed and unsigned comparisons coincide  -/
BitVec.slt_eq_ult_of_msb_eq : ∀ {w : ℕ} {x y : BitVec w}, x.msb = y.msb → x.slt y = x.ult y
-- Mathlib.Condensed.Light.Sequence
_private.Mathlib.Condensed.Light.Sequence.0.InternalProjectivityProof.LightProfinite.fibreIncl : {X Y : LightProfinite} → (y : ↑Y.toTop) → (f : X ⟶ Y) → InternalProjectivityProof.LightProfinite.fibre✝ y f ⟶ X
-- Mathlib.Algebra.Algebra.Basic
/-- If `R` embeds faithfully into `A` and `G` satisfies `SMulDistribClass G R A`, then
the `SMul` of `G` on `R` extends to a `MulSemiringAction`.  -/
mulSemiringActionOfSmulDistribClass : (R : Type u_1) →
  (A : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra R A] →
          [FaithfulSMul R A] →
            (G : Type u_3) →
              [inst_4 : Monoid G] →
                [inst_5 : MulSemiringAction G A] →
                  [inst_6 : SMul G R] → [SMulDistribClass G R A] → MulSemiringAction G R
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.instWeakEquivalenceI₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.Cylinder A)
  [(HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty]
  [(HomotopicalAlgebra.weakEquivalences C).ContainsIdentities], HomotopicalAlgebra.WeakEquivalence P.i₀
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
/-- Free additive groups are torsion free, i.e., scalar multiplication by every
non-zero element `n : ℕ` is injective. See the instance for free groups for an overview over the
proof.  -/
FreeAddGroup.instIsAddTorsionFree : ∀ {α : Type u}, IsAddTorsionFree (FreeAddGroup α)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.eta : ∀ {R : Type u} [inst : Semiring R] (f : Polynomial R), { toFinsupp := f.toFinsupp } = f
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.isBounded_preimage_toSnowflaking_iff : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : Bornology X] {s : Set (Metric.Snowflaking X α hα₀ hα₁)},
  Bornology.IsBounded (⇑Metric.Snowflaking.toSnowflaking ⁻¹' s) ↔ Bornology.IsBounded s
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.inv_hom_apply : ∀ {A B : ProfiniteGrp.{u}} (e : A ≅ B) (x : ↑A.toProfinite.toTop),
  (ProfiniteGrp.Hom.hom e.inv) ((ProfiniteGrp.Hom.hom e.hom) x) = x
-- Mathlib.Order.WithBot
WithTop.eq_of_forall_coe_le_iff : ∀ {α : Type u_1} [inst : PartialOrder α] {x y : WithTop α} [NoTopOrder α], (∀ (a : α), ↑a ≤ x ↔ ↑a ≤ y) → x = y
-- Mathlib.Order.Interval.Set.ProjIcc
Set.projIci_surjective : ∀ {α : Type u_1} [inst : LinearOrder α] {a : α}, Function.Surjective (Set.projIci a)
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Embedding.comap_eq : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (f : H ↪g G), SimpleGraph.comap (⇑f) G = H
-- Mathlib.Topology.VectorBundle.Basic
VectorPrebundle.mk.sizeOf_spec : ∀ {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 : (x : B) → TopologicalSpace (E x)]
  [inst_7 : SizeOf R] [inst_8 : SizeOf B] [inst_9 : SizeOf F] [inst_10 : (a : B) → SizeOf (E a)]
  (pretrivializationAtlas : Set (Bundle.Pretrivialization F Bundle.TotalSpace.proj))
  (pretrivialization_linear' : ∀ e ∈ pretrivializationAtlas, Bundle.Pretrivialization.IsLinear R e)
  (pretrivializationAt : B → Bundle.Pretrivialization F Bundle.TotalSpace.proj)
  (mem_base_pretrivializationAt : ∀ (x : B), x ∈ (pretrivializationAt x).baseSet)
  (pretrivialization_mem_atlas : ∀ (x : B), pretrivializationAt x ∈ pretrivializationAtlas)
  (exists_coordChange :
    ∀ e ∈ pretrivializationAtlas,
      ∀ e' ∈ pretrivializationAtlas,
        ∃ f,
          ContinuousOn f (e.baseSet ∩ e'.baseSet) ∧
            ∀ b ∈ e.baseSet ∩ e'.baseSet, ∀ (v : F), (f b) v = (↑e' ⟨b, e.symm b v⟩).2)
  (totalSpaceMk_isInducing : ∀ (b : B), Topology.IsInducing (↑(pretrivializationAt b) ∘ Bundle.TotalSpace.mk b)),
  sizeOf
      { pretrivializationAtlas := pretrivializationAtlas, pretrivialization_linear' := pretrivialization_linear',
        pretrivializationAt := pretrivializationAt, mem_base_pretrivializationAt := mem_base_pretrivializationAt,
        pretrivialization_mem_atlas := pretrivialization_mem_atlas, exists_coordChange := exists_coordChange,
        totalSpaceMk_isInducing := totalSpaceMk_isInducing } =
    1
-- Mathlib.Topology.Sheaves.Presheaf
IsOpenMap.pullbackIso_hom_app_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X Y : TopCat}
  {f : X ⟶ Y} (hf : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)) (X_1 : TopCat.Presheaf C Y)
  (X_2 : (TopologicalSpace.Opens ↑X)ᵒᵖ),
  (hf.pullbackIso.hom.app X_1).app X_2 = (TopCat.Presheaf.pullbackObjObjOfImageOpen f X_1 (Opposite.unop X_2) ⋯).hom
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.two_mul_le_exp : ∀ {x : ℝ}, 2 * x ≤ Real.exp x
-- Mathlib.Data.Seq.Basic
Stream'.Seq1.bind.eq_1 : ∀ {α : Type u} {β : Type v} (s : Stream'.Seq1 α) (f : α → Stream'.Seq1 β), s.bind f = (Stream'.Seq1.map f s).join
-- Mathlib.Data.ENNReal.Basic
ENNReal.toReal_ne_zero : ∀ {a : ENNReal}, a.toReal ≠ 0 ↔ a ≠ 0 ∧ a ≠ ⊤
-- Mathlib.SetTheory.ZFC.Ordinal
ZFSet.isTransitive_empty : ∅.IsTransitive
-- Mathlib.NumberTheory.MulChar.Lemmas
/-- The group of multiplicative characters on a finite monoid `M` with cyclic unit group `Mˣ`
of order `n` is isomorphic to the group of `n`th roots of unity in the target `R`.  -/
MulChar.equiv_rootsOfUnity : (M : Type u_1) →
  [inst : CommMonoid M] →
    [inst_1 : Fintype M] →
      [inst_2 : DecidableEq M] →
        (R : Type u_2) →
          [inst_3 : CommMonoidWithZero R] →
            [inst_cyc : IsCyclic Mˣ] → MulChar M R ≃* ↥(rootsOfUnity (Fintype.card Mˣ) R)
-- Init.Data.Option.Lemmas
Option.none_beq_some : ∀ {α : Type u_1} [inst : BEq α] (a : α), (none == some a) = false
-- Mathlib.Data.Set.Lattice.Image
Set.image2_iUnion_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_5} (f : α → β → γ) (s : ι → Set α) (t : Set β),
  Set.image2 f (⋃ i, s i) t = ⋃ i, Set.image2 f (s i) t