mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.Weight.instDecidablePredIsNonZero : {R : Type u_2} →
  {L : Type u_3} →
    {M : Type u_4} →
      [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] →
                    [inst_7 : LieRing.IsNilpotent L] → DecidablePred LieModule.Weight.IsNonZero
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.subset : ∀ {α : Type u} {s : Set α}, s.Finite → ∀ {t : Set α}, t ⊆ s → t.Finite
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, (t₁ ∪ t₂).getKey? k = (t₂.getKey? k).or (t₁.getKey? k)
-- Mathlib.Data.Set.Finite.Lattice
Set.fintypesUnion : {α : Type u} → [DecidableEq α] → {s : Set (Set α)} → [Fintype ↑s] → [H : (t : ↑s) → Fintype ↑↑t] → Fintype ↑(⋃₀ s)
-- Init.GrindInstances.ToInt
Lean.Grind.instMulInt16SintOfNatNat : Lean.Grind.ToInt.Mul Int16 (Lean.Grind.IntInterval.sint 16)
-- Mathlib.MeasureTheory.Measure.Dirac
/-- The dirac measure.  -/
MeasureTheory.Measure.dirac : {α : Type u_1} → [inst : MeasurableSpace α] → α → MeasureTheory.Measure α
-- Mathlib.Topology.Algebra.Ring.Basic
/-- The forgetful functor from ring topologies on `a` to additive group topologies on `a`.  -/
RingTopology.toAddGroupTopology : {R : Type u_1} → [inst : Ring R] → RingTopology R → AddGroupTopology R
-- Init.Data.List.Range
List.getElem_range' : ∀ {n m step i : ℕ} (H : i < (List.range' n m step).length), (List.range' n m step)[i] = n + step * i
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyGE?.go.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (best : Option α),
  Std.DTreeMap.Internal.Impl.getKeyGE?.go k best Std.DTreeMap.Internal.Impl.leaf = best
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.continuousOn_of_dominated : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {X : Type u_6} [inst_2 : TopologicalSpace X] [FirstCountableTopology X] {F : X → α → G}
  {bound : α → ℝ} {s : Set X},
  (∀ x ∈ s, MeasureTheory.AEStronglyMeasurable (F x) μ) →
    (∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a) →
      MeasureTheory.Integrable bound μ →
        (∀ᵐ (a : α) ∂μ, ContinuousOn (fun x => F x a) s) → ContinuousOn (fun x => ∫ (a : α), F x a ∂μ) s
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.ofIsoSelf_inv : ∀ {R : Type u} [inst : CommRing R] (M : CommBialgCat R), M.ofIsoSelf.inv = CategoryTheory.CategoryStruct.id M
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
EisensteinSeries.G2_eq_tsum_symmetricIco : ∀ (z : UpperHalfPlane),
  EisensteinSeries.G2 z = ∑'[SummationFilter.symmetricIco ℤ] (m : ℤ), EisensteinSeries.e2Summand m z
-- Lean.Expr
Lean.Expr.updateLambdaE! : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.hasHomology_of_preserves : ∀ {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 : CategoryTheory.ShortComplex C)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [S.HasHomology] [F.PreservesLeftHomologyOf S]
  [F.PreservesRightHomologyOf S], (S.map F).HasHomology
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
TopologicalSpace.complete_completelyMetrizableMetric : ∀ (X : Type u_3) [ht : TopologicalSpace X] [h : TopologicalSpace.IsCompletelyMetrizableSpace X], CompleteSpace X
-- Lean.Language.Lean.Types
Lean.Language.Lean.HeaderProcessedState.mk : Lean.Elab.Command.State →
  Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot → Lean.Language.Lean.HeaderProcessedState
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- Eta-expanded form of `HasDerivWithinAt.const_smul` -/
HasDerivWithinAt.fun_const_smul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜} {R : Type u_2} [inst_3 : Monoid R]
  [inst_4 : DistribMulAction R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] (c : R),
  HasDerivWithinAt f f' s x → HasDerivWithinAt (fun i => c • f i) (c • f') s x
-- Mathlib.Algebra.Category.Grp.FiniteGrp
/-- The morphism in `FiniteAddGrp`, induced from a morphism of the category `AddGrpCat`  -/
FiniteAddGrp.ofHom : {X Y : Type u} →
  [inst : AddGroup X] →
    [inst_1 : Finite X] →
      [inst_2 : AddGroup Y] → [inst_3 : Finite Y] → (X →+ Y) → (FiniteAddGrp.of X ⟶ FiniteAddGrp.of Y)
-- Init.Data.Array.Monadic
_private.Init.Data.Array.Monadic.0.List.foldlM_filterMap.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match some b with
    | some b => h_1 b
    | none => h_2 ()) =
    h_1 b
-- Mathlib.NumberTheory.Transcendental.Liouville.Residual
/-- The set of Liouville numbers is a residual set.  -/
eventually_residual_liouville : ∀ᶠ (x : ℝ) in residual ℝ, Liouville x
-- Mathlib.Topology.Constructions.SumProd
/-- Product of two homeomorphisms.  -/
Homeomorph.prodCongr : {X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {X' : Type u_5} →
          {Y' : Type u_6} →
            [inst_2 : TopologicalSpace X'] → [inst_3 : TopologicalSpace Y'] → X ≃ₜ X' → Y ≃ₜ Y' → X × Y ≃ₜ X' × Y'
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.instInhabited : {α : Type u_2} → [inst : TopologicalSpace α] → Inhabited (TopologicalSpace.Clopens α)
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Natural transformations between functors lift to additive monoid objects.  -/
CategoryTheory.Functor.mapAddMonNatTrans : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F F' : CategoryTheory.Functor C D} →
              [inst_4 : F.LaxMonoidal] →
                [inst_5 : F'.LaxMonoidal] →
                  (f : F ⟶ F') → [CategoryTheory.NatTrans.IsMonoidal f] → F.mapAddMon ⟶ F'.mapAddMon
-- Mathlib.Data.DFinsupp.WellFounded
DFinsupp.Lex.wellFounded' : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop},
  (∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0) →
    (∀ (i : ι), WellFounded (s i)) →
      ∀ [Std.Trichotomous r], WellFounded (Function.swap r) → WellFounded (DFinsupp.Lex r s)
-- Mathlib.NumberTheory.ModularForms.NormTrace
CuspForm.coe_trace : ∀ {𝒢 : Subgroup (GL (Fin 2) ℝ)} (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1} (f : F) [inst : FunLike F UpperHalfPlane ℂ]
  {k : ℤ} [inst_1 : 𝒢.IsFiniteRelIndex ℋ] [inst_2 : CuspFormClass F 𝒢 k],
  ⇑(CuspForm.trace ℋ f) = ∑ q, SlashInvariantForm.quotientFunc f q
-- Mathlib.Order.Hom.Basic
OrderIso.orderIsoCongr_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : LE α] [inst_1 : LE β] [inst_2 : LE γ]
  [inst_3 : LE δ] (f : α ≃o γ) (g : β ≃o δ) (h : α ≃o β), (f.orderIsoCongr g) h = (f.symm.trans h).trans g
-- Mathlib.CategoryTheory.MorphismProperty.Retract
CategoryTheory.MorphismProperty.IsStableUnderRetracts.epimorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.MorphismProperty.epimorphisms C).IsStableUnderRetracts
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
/-- Lebesgue integral of a bounded function over a set of finite measure is finite.
Note that this lemma assumes no regularity of either `f` or `s`.  -/
MeasureTheory.setLIntegral_lt_top_of_bddAbove : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  μ s ≠ ⊤ → ∀ {f : α → NNReal}, BddAbove (f '' s) → ∫⁻ (x : α) in s, ↑(f x) ∂μ < ⊤
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
/-- If `f : ℕ → M` is summable, then the partial sums `∑ i ∈ range n, f i` converge
to `∑' i, f i`.  -/
Summable.tendsto_sum_tsum_nat : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {f : ℕ → M},
  Summable f → Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds (∑' (i : ℕ), f i))
-- Mathlib.Algebra.Quandle
Quandle.conj_act_eq_conj : ∀ {G : Type u_2} [inst : Group G] (x y : Quandle.Conj G), Shelf.act x y = x * y * x⁻¹
-- Mathlib.RingTheory.Int.Basic
Int.sq_of_isCoprime : ∀ {a b c : ℤ}, IsCoprime a b → a * b = c ^ 2 → ∃ a0, a = a0 ^ 2 ∨ a = -a0 ^ 2
-- Mathlib.GroupTheory.OreLocalization.Basic
_private.Mathlib.GroupTheory.OreLocalization.Basic.0.OreLocalization.smul'_char : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : MulAction R X] (r₁ : R) (r₂ : X) (s₁ s₂ u : ↥S) (v : R),
  ↑u * r₁ = v * ↑s₂ → OreLocalization.smul'✝ r₁ s₁ r₂ s₂ = v • r₂ /ₒ (u * s₁)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.maxD_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k fallback : α},
  (t.insert k).maxD fallback = t.max?.elim k fun k' => if cmp k' k = Ordering.lt then k else k'
-- Std.Data.ByteSlice
/-- The starting index of the region of interest (inclusive).
 -/
ByteSlice.start : ByteSlice → ℕ
-- Mathlib.LinearAlgebra.Matrix.Basis
LinearMap.toMatrix_eq_basisToMatrix : ∀ {ι : Type u_1} {κ : Type u_3} {R : Type u_5} {M : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {N : Type u_9} [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (b : Module.Basis ι R M)
  (c : Module.Basis κ R N) (f : M →ₗ[R] N) [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] [inst_7 : Finite κ],
  (LinearMap.toMatrix b c) f = c.toMatrix (⇑f ∘ ⇑b)
-- Mathlib.Topology.SeparatedMap
/-- A function from a topological space `X` to a type `Y` is a separated map if any two distinct
points in `X` with the same image in `Y` can be separated by open neighborhoods.  -/
IsSeparatedMap : {X : Type u_1} → {Y : Sort u_2} → [TopologicalSpace X] → (X → Y) → Prop
-- Init.Data.SInt.Bitwise
Int32.xor_eq_zero_iff : ∀ {a b : Int32}, a ^^^ b = 0 ↔ a = b
-- Mathlib.Combinatorics.SetFamily.Shadow
/-- Being in the shadow of `𝒜` means we have a superset in `𝒜`.  -/
Finset.exists_subset_of_mem_shadow : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {t : Finset α}, t ∈ 𝒜.shadow → ∃ s ∈ 𝒜, t ⊆ s
-- Mathlib.Topology.Sets.CompactOpenCovered
/-- Being compact open covered descends along refinements if the spaces are prespectral.  -/
IsCompactOpenCovered.of_comp : ∀ {S : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {f : (i : ι) → X i → S} [inst : (i : ι) → TopologicalSpace (X i)]
  [∀ (i : ι), PrespectralSpace (X i)] [inst_2 : TopologicalSpace S] {σ : Type u_4} {Y : σ → Type u_5}
  [inst_3 : (i : σ) → TopologicalSpace (Y i)] (g : (i : σ) → Y i → S) {a : σ → ι} (t : (i : σ) → Y i → X (a i)),
  (∀ (i : σ), Continuous (t i)) →
    (∀ (i : σ), g i = f (a i) ∘ t i) →
      (∀ (i : ι), Continuous (f i)) → ∀ {U : Set S}, IsOpen U → IsCompactOpenCovered g U → IsCompactOpenCovered f U
-- Mathlib.GroupTheory.Sylow
/-- If `H` is a subgroup of `G` of cardinality `p ^ n`,
then `H` is contained in a subgroup of cardinality `p ^ (n + 1)`
if `p ^ (n + 1)` divides the cardinality of `G`  -/
Sylow.exists_subgroup_card_pow_succ : ∀ {G : Type u} [inst : Group G] [Finite G] {p n : ℕ} [hp : Fact (Nat.Prime p)],
  p ^ (n + 1) ∣ Nat.card G → ∀ {H : Subgroup G}, Nat.card ↥H = p ^ n → ∃ K, Nat.card ↥K = p ^ (n + 1) ∧ H ≤ K
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.mk_tensor : ∀ {C : Type u} {X₁ Y₁ X₂ Y₂ : CategoryTheory.FreeMonoidalCategory C} (f : X₁.Hom Y₁) (g : X₂.Hom Y₂),
  ⟦f.tensor g⟧ = CategoryTheory.MonoidalCategoryStruct.tensorHom ⟦f⟧ ⟦g⟧
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R}
  {x y : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v}, x = y ↔ x.toCompletion = y.toCompletion
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_eq_some_getKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a fallback : α},
  a ∈ t → t.getKey? a = some (t.getKeyD a fallback)
-- Mathlib.Data.Real.ConjExponents
ENNReal.HolderTriple.toReal_iff : ∀ {p q : ENNReal} (r : ENNReal),
  0 < p.toReal → 0 < q.toReal → (p.toReal.HolderTriple q.toReal r.toReal ↔ p.HolderTriple q r)
-- Batteries.Tactic.Lint.Basic
/-- Defines the user attribute `nolint` for skipping `#lint`  -/
Batteries.Tactic.Lint.nolintAttr : Lean.ParametricAttribute (Array Lean.Name)
-- Mathlib.Control.Random
Random.instULiftOfULiftable : {m : Type u → Type u_1} →
  {m' : Type (max v u) → Type u_2} → {α : Type u} → [ULiftable m m'] → [Random m α] → Random m' (ULift.{v, u} α)
-- Mathlib.Algebra.Group.Finsupp
Finsupp.instIsCancelAdd : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] [IsCancelAdd M], IsCancelAdd (ι →₀ M)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.toSubgraph_cons_nil_eq_subgraphOfAdj : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v),
  (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil).toSubgraph = G.subgraphOfAdj h
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Prod.swapIsEquivalence : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D],
  (CategoryTheory.Prod.swap C D).IsEquivalence
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_insert : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} {a : ι} [inst : AddCommMonoid M] {f : ι → M} [inst_1 : DecidableEq ι],
  a ∉ s → ∑ x ∈ insert a s, f x = f a + ∑ x ∈ s, f x
-- Mathlib.Dynamics.Ergodic.AddCircle
AddCircle.ergodic_zsmul_add : ∀ {T : ℝ} [hT : Fact (0 < T)] (x : AddCircle T) {n : ℤ}, 1 < |n| → Ergodic (fun y => n • y + x) MeasureTheory.volume
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- This is a slightly more convenient method to verify that a pullback cone is a limit cone. It
only asks for a proof of facts that carry any mathematical content  -/
CategoryTheory.Limits.PullbackCone.isLimitAux : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f : X ⟶ Z} →
        {g : Y ⟶ Z} →
          (t : CategoryTheory.Limits.PullbackCone f g) →
            (lift : (s : CategoryTheory.Limits.PullbackCone f g) → s.pt ⟶ t.pt) →
              (∀ (s : CategoryTheory.Limits.PullbackCone f g),
                  CategoryTheory.CategoryStruct.comp (lift s) t.fst = s.fst) →
                (∀ (s : CategoryTheory.Limits.PullbackCone f g),
                    CategoryTheory.CategoryStruct.comp (lift s) t.snd = s.snd) →
                  (∀ (s : CategoryTheory.Limits.PullbackCone f g) (m : s.pt ⟶ t.pt),
                      (∀ (j : CategoryTheory.Limits.WalkingCospan),
                          CategoryTheory.CategoryStruct.comp m (t.π.app j) = s.π.app j) →
                        m = lift s) →
                    CategoryTheory.Limits.IsLimit t
-- Mathlib.CategoryTheory.Action.Basic
Action.resComp_hom_app_hom : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} {H : Type u_4} {K : Type u_5}
  [inst_1 : Monoid G] [inst_2 : Monoid H] [inst_3 : Monoid K] (f : G →* H) (g : H →* K) (X : Action V K),
  ((Action.resComp V f g).hom.app X).hom = CategoryTheory.CategoryStruct.id X.V
-- Mathlib.Algebra.Ring.Commute
/-- **Alias** of `sub_sq`. -/
sub_pow_two : ∀ {R : Type u} [inst : CommRing R] (a b : R), (a - b) ^ 2 = a ^ 2 - 2 * a * b + b ^ 2
-- Mathlib.CategoryTheory.Subobject.Lattice
/-- `map f` sends `⊥ : MonoOver X` to `⊥ : MonoOver Y`.  -/
CategoryTheory.MonoOver.mapBot : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      [inst_1 : CategoryTheory.Limits.HasInitial C] →
        [inst_2 : CategoryTheory.Limits.InitialMonoClass C] →
          (f : X ⟶ Y) → [inst_3 : CategoryTheory.Mono f] → (CategoryTheory.MonoOver.map f).obj ⊥ ≅ ⊥
-- Mathlib.Data.Finset.Image
Finset.map_inj : ∀ {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s₁ s₂ : Finset α}, Finset.map f s₁ = Finset.map f s₂ ↔ s₁ = s₂
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.exp_pi_div_two_mul_I : Complex.exp (↑Real.pi / 2 * Complex.I) = Complex.I
-- Mathlib.Data.Sym.Basic
/-- Note: `Sym.map_id` is not simp-normal, as simp ends up unfolding `id` with `Sym.map_congr`  -/
Sym.map_id' : ∀ {α : Type u_3} {n : ℕ} (s : Sym α n), Sym.map (fun x => x) s = s
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- the compatibility between the given section and retraction  -/
CategoryTheory.ShortComplex.Splitting.id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (self : S.Splitting),
  CategoryTheory.CategoryStruct.comp self.r S.f + CategoryTheory.CategoryStruct.comp S.g self.s =
    CategoryTheory.CategoryStruct.id S.X₂
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.instSubgroupClass : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G], SubgroupClass (OpenSubgroup G) G
-- Mathlib.Logic.Equiv.Fin.Basic
/-- An embedding `e : Fin (n+1) ↪ ι` corresponds to an embedding `f : Fin n ↪ ι` (corresponding
the last `n` coordinates of `e`) together with a value not taken by `f` (corresponding to `e 0`).  -/
Equiv.embeddingFinSucc : (n : ℕ) → (ι : Type u_1) → (Fin (n + 1) ↪ ι) ≃ (e : Fin n ↪ ι) × { i // i ∉ Set.range ⇑e }
-- Aesop.Frontend.Extension.Init
Aesop.getDefaultRuleSetNames : IO (Std.HashSet Lean.Name)
-- Lean.Meta.Basic
Lean.Meta.instHashableExprConfigCacheKey : Hashable Lean.Meta.ExprConfigCacheKey
-- Lean.Elab.PreDefinition.FixedParams
/-- Number of fixed parameters  -/
Lean.Elab.FixedParamPerms.numFixed : Lean.Elab.FixedParamPerms → ℕ
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.mk'_edge : ∀ {X : SSet} (s : X.obj (Opposite.op { len := 1 })), (SSet.Edge.mk' s).edge = s
-- Mathlib.Analysis.Normed.Operator.Mul
/-- Every (unital) normed algebra such that `‖1‖ = 1` is a `RegularNormedAlgebra`.  -/
NormedAlgebra.instRegularNormedAlgebra : ∀ {𝕜 : Type u_4} {R : Type u_5} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedRing R]
  [inst_2 : NormedAlgebra 𝕜 R] [NormOneClass R], RegularNormedAlgebra 𝕜 R
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.exists_measurable_superset₂ : ∀ {α : Type u_1} [inst : MeasurableSpace α] (μ ν : MeasureTheory.Measure α) (s : Set α),
  ∃ t, s ⊆ t ∧ MeasurableSet t ∧ μ t = μ s ∧ ν t = ν s
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.toProp.eq_3 : ∀ (K : Type u_2) [inst : Add K] [inst_1 : Mul K] [inst_2 : Neg K] [inst_3 : Zero K] [inst_4 : One K],
  FirstOrder.Field.FieldAxiom.toProp K FirstOrder.Field.FieldAxiom.negAddCancel = ∀ (x : K), -x + x = 0
-- Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
BoundedContinuousFunction.tendsto_integral_of_forall_limsup_integral_le_integral : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [OpensMeasurableSpace X] {ι : Type u_2}
  {L : Filter ι} {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] {μs : ι → MeasureTheory.Measure X}
  [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)],
  (∀ (f : BoundedContinuousFunction X ℝ), 0 ≤ f → Filter.limsup (fun i => ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ) →
    ∀ (f : BoundedContinuousFunction X ℝ), Filter.Tendsto (fun i => ∫ (x : X), f x ∂μs i) L (nhds (∫ (x : X), f x ∂μ))
-- Batteries.Data.Fin.Coding
Fin.getRepr.congr_simp : ∀ {n : ℕ} (s s_1 : Setoid (Fin n)),
  s = s_1 →
    ∀ {inst : DecidableRel ⇑s} [inst_1 : DecidableRel ⇑s_1] (x x_1 : Fin n),
      x = x_1 → Fin.getRepr s x = Fin.getRepr s_1 x_1
-- Lean.Widget.TaggedText
Lean.Widget.TaggedText.brecOn_1.eq : ∀ {α : Type u} {motive_1 : Lean.Widget.TaggedText α → Sort u_1} {motive_2 : Array (Lean.Widget.TaggedText α) → Sort u_1}
  {motive_3 : List (Lean.Widget.TaggedText α) → Sort u_1} (t : Array (Lean.Widget.TaggedText α))
  (F_1 : (t : Lean.Widget.TaggedText α) → t.below → motive_1 t)
  (F_2 : (t : Array (Lean.Widget.TaggedText α)) → Lean.Widget.TaggedText.below_1 t → motive_2 t)
  (F_3 : (t : List (Lean.Widget.TaggedText α)) → Lean.Widget.TaggedText.below_2 t → motive_3 t),
  Lean.Widget.TaggedText.brecOn_1 t F_1 F_2 F_3 = F_2 t (Lean.Widget.TaggedText.brecOn_1.go t F_1 F_2 F_3).2
-- Mathlib.Combinatorics.Graph.Basic
Graph.IsLoopAt.inc : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β}, G.IsLoopAt e x → G.Inc e x
-- Mathlib.Algebra.Notation.Support
Pi.support_single_of_ne : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Zero M] {i : ι} {a : M},
  a ≠ 0 → Function.support (Pi.single i a) = {i}
-- Std.Time.Zoned.TimeZone
/-- A zeroed `Timezone` representing UTC (no offset).
 -/
Std.Time.TimeZone.UTC : Std.Time.TimeZone
-- Mathlib.Logic.Equiv.Set
Equiv.Set.union_apply_right : ∀ {α : Type u_3} {s t : Set α} [inst : DecidablePred fun x => x ∈ s] (H : Disjoint s t) {a : ↑(s ∪ t)} (ha : ↑a ∈ t),
  (Equiv.Set.union H) a = Sum.inr ⟨↑a, ha⟩
-- Mathlib.Algebra.Polynomial.Mirror
Polynomial.mirror_leadingCoeff : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R), p.mirror.leadingCoeff = p.trailingCoeff
-- Mathlib.MeasureTheory.OuterMeasure.Defs
MeasureTheory.OuterMeasure.instOuterMeasureClass : ∀ {α : Type u_1}, MeasureTheory.OuterMeasureClass (MeasureTheory.OuterMeasure α) α
-- Init.Data.List.Scan.Lemmas
List.scanrM_nil : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} [inst : Monad m] {f : α → β → m β},
  List.scanrM f init [] = pure [init]
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomMulAct.smul_Lp_add : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : SMul M α] [inst_3 : MeasureTheory.SMulInvariantMeasure M α μ]
  [inst_4 : MeasurableConstSMul M α] (c : Mᵈᵐᵃ) (f g : ↥(MeasureTheory.Lp E p μ)), c • (f + g) = c • f + c • g
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- Around each point, there are only finitely many nonzero bump functions in the family.  -/
SmoothBumpCovering.locallyFinite' : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] [inst_5 : FiniteDimensional ℝ E] {s : optParam (Set M) Set.univ}
  (self : SmoothBumpCovering ι I M s), LocallyFinite fun i => Function.support ↑(self.toFun i)
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- Postcomposing `f` with `Prod.fst` is `C^n` at `x`  -/
ContDiffWithinAt.fst : ∀ {𝕜 : 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} {n : WithTop ℕ∞} {f : E → F × G} {x : E},
  ContDiffWithinAt 𝕜 n f s x → ContDiffWithinAt 𝕜 n (fun x => (f x).1) s x
-- Std.Time.Format.Modifier
/-- Truncated to `digits` digits (truncated, not rounded)
 -/
Std.Time.Fraction.truncated : ℕ → Std.Time.Fraction
-- Mathlib.SetTheory.Ordinal.Veblen
/-- `Γ₀` is the limit of `0`, `veblen 0 0`, `veblen (veblen 0 0) 0`, …  -/
Ordinal.lt_gamma_zero : ∀ {o : Ordinal.{u}}, o < Ordinal.gamma 0 ↔ ∃ n, o < (fun a => Ordinal.veblen a 0)^[n] 0