mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.AdicCauchySequence.mk_coe : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (f : ℕ → M) (h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]) (a : ℕ),
  ↑(AdicCompletion.AdicCauchySequence.mk I M f h) a = f a
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.orElse : {α : Type} →
  Lean.Elab.Tactic.Grind.GrindTacticM α →
    (Unit → Lean.Elab.Tactic.Grind.GrindTacticM α) → Lean.Elab.Tactic.Grind.GrindTacticM α
-- Init.Data.List.Lemmas
/-- A reasoning principle for proving propositions about the result of `List.foldl` by establishing an
invariant that is true for the initial data and preserved by the operation being folded.

Because the motive can return a type in any sort, this function may be used to construct data as
well as to prove propositions.

Example:
```lean example
example {xs : List Nat} : xs.foldl (· + ·) 1 > 0 := by
  apply List.foldlRecOn
  . show 0 < 1; trivial
  . show ∀ (b : Nat), 0 < b → ∀ (a : Nat), a ∈ xs → 0 < b + a
    intros; omega
```
 -/
List.foldlRecOn : {β : Type u_1} →
  {α : Type u_2} →
    {motive : β → Sort u_3} →
      (l : List α) →
        (op : β → α → β) →
          {b : β} → motive b → ((b : β) → motive b → (a : α) → a ∈ l → motive (op b a)) → motive (List.foldl op b l)
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.u_eq : ∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
  GaloisConnection l u → ∀ {z : α} {y : β}, u y = z ↔ ∀ (x : α), x ≤ z ↔ l x ≤ y
-- Mathlib.Algebra.Order.Ring.Abs
mabs_zpow : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : LinearOrder α] [IsOrderedMonoid α] (n : ℤ) (a : α),
  |a ^ n|ₘ = |a|ₘ ^ |n|
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.surjOn_sin : Set.SurjOn Real.sin (Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) (Set.Icc (-1) 1)
-- Mathlib.GroupTheory.Transfer
/-- **Burnside's normal p-complement theorem**: If `N(P) ≤ C(P)`, then `P` has a normal
complement.  -/
MonoidHom.ker_transferSylow_isComplement' : ∀ {G : Type u_1} [inst : Group G] {p : ℕ} (P : Sylow p G) (hP : Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P)
  [Fact (Nat.Prime p)] [Finite (Sylow p G)] [inst_3 : (↑P).FiniteIndex],
  (MonoidHom.transferSylow P hP).ker.IsComplement' ↑P
-- Mathlib.Topology.Bases
TopologicalSpace.isOpen_of_mem_countableBasis : ∀ {α : Type u} [t : TopologicalSpace α] [inst : SecondCountableTopology α] {s : Set α},
  s ∈ TopologicalSpace.countableBasis α → IsOpen s
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.Algebra.of_apply : ∀ {R : Type u_1} {ι : Type u_2} [inst : Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : CommSemiring R]
  [inst_5 : (i : ι) → Semiring (G i)] [inst_6 : (i : ι) → Algebra R (G i)]
  [inst_7 : ∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)] [inst_8 : Nonempty ι] (i : ι) (x : G i),
  (DirectLimit.Algebra.of G f i) x = ⟦⟨i, x⟩⟧
-- Mathlib.CategoryTheory.Triangulated.Adjunction
CategoryTheory.Equivalence.IsTriangulated.instIsTriangulatedInverse : ∀ {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.HasZeroObject C]
  [inst_3 : CategoryTheory.Limits.HasZeroObject D] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : CategoryTheory.Preadditive D] [inst_6 : CategoryTheory.HasShift C ℤ] [inst_7 : CategoryTheory.HasShift D ℤ]
  [inst_8 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_10 : CategoryTheory.Pretriangulated C]
  [inst_11 : CategoryTheory.Pretriangulated D] (E : C ≌ D) [inst_12 : E.functor.CommShift ℤ]
  [inst_13 : E.inverse.CommShift ℤ] [E.IsTriangulated], E.inverse.IsTriangulated
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_lt_top_of_nonneg : ∀ {x : ENNReal} {y : ℝ}, 0 ≤ y → x ≠ ⊤ → x ^ y < ⊤
-- Lean.Elab.Tactic.Conv.Basic
/-- Given `lhs`, runs the `conv` tactic with the goal `⊢ lhs = ?rhs`.
`conv` should produce no remaining goals that are not solvable with refl.
Returns a pair of instantiated expressions `(?rhs, ?p)` where `?p : lhs = ?rhs`.  -/
Lean.Elab.Tactic.Conv.convert : Lean.Expr → Lean.Elab.Tactic.TacticM Unit → Lean.Elab.Tactic.TacticM (Lean.Expr × Lean.Expr)
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.dist_triangle : ∀ {E : ℕ → Type u_1} (x y z : (n : ℕ) → E n), dist x z ≤ dist x y + dist y z
-- Lean.Parser.Extra
Lean.Parser.sepByIndent : Lean.Parser.Parser →
  (sep : String) → optParam Lean.Parser.Parser (Lean.Parser.symbol sep) → optParam Bool false → Lean.Parser.Parser
-- Mathlib.Topology.MetricSpace.CantorScheme
/-- A scheme on a complete space with vanishing diameter
such that each set contains the closure of its children
induces a total map.  -/
CantorScheme.ClosureAntitone.map_of_vanishingDiam : ∀ {β : Type u_1} {α : Type u_2} {A : List β → Set α} [inst : PseudoMetricSpace α] [CompleteSpace α],
  CantorScheme.VanishingDiam A →
    CantorScheme.ClosureAntitone A → (∀ (l : List β), (A l).Nonempty) → (CantorScheme.inducedMap A).fst = Set.univ
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.univ_mul_of_one_mem : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] {t : Finset α} [inst_2 : Fintype α],
  1 ∈ t → Finset.univ * t = Finset.univ
-- Init.Core
/-- Like `Quotient.liftOn q f h` but allows `f a` to "know" that `q = Quotient.mk s a`.
 -/
Quotient.pliftOn : {β : Sort u_1} →
  {α : Sort u} →
    {s : Setoid α} →
      (q : Quotient s) →
        (f : (a : α) → q = ⟦a⟧ → β) → (∀ (a b : α) (h : q = ⟦a⟧) (h' : q = ⟦b⟧), a ≈ b → f a h = f b h') → β
-- Mathlib.Analysis.Fourier.ZMod
ZMod.dft.eq_1 : ∀ {N : ℕ} [inst : NeZero N] {E : Type u_1} [inst_1 : AddCommGroup E] [inst_2 : Module ℂ E],
  ZMod.dft =
    { toFun := ZMod.auxDFT✝, map_add' := ⋯, map_smul' := ⋯, invFun := fun Φ k => (↑N)⁻¹ • ZMod.auxDFT✝ Φ (-k),
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.LinearAlgebra.Dual.Basis
Module.DualBases.mem_of_mem_span : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {e : ι → M} {ε : ι → Module.Dual R M},
  Module.DualBases e ε → ∀ {H : Set ι} {x : M}, x ∈ Submodule.span R (e '' H) → ∀ (i : ι), (ε i) x ≠ 0 → i ∈ H
-- Mathlib.Combinatorics.SimpleGraph.Partition
SimpleGraph.Partition.mk.inj : ∀ {V : Type u} {G : SimpleGraph V} {parts : Set (Set V)} {isPartition : Setoid.IsPartition parts}
  {independent : ∀ s ∈ parts, IsAntichain G.Adj s} {parts_1 : Set (Set V)} {isPartition_1 : Setoid.IsPartition parts_1}
  {independent_1 : ∀ s ∈ parts_1, IsAntichain G.Adj s},
  { parts := parts, isPartition := isPartition, independent := independent } =
      { parts := parts_1, isPartition := isPartition_1, independent := independent_1 } →
    parts = parts_1
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
/-- Interpret a `CStarMatrix m n A` as a continuous linear map acting on `C⋆ᵐᵒᵈ (n → A)`. This
version is specialized to the case `m = n` and is bundled as a non-unital algebra homomorphism.  -/
CStarMatrix.toCLMNonUnitalAlgHom : {n : Type u_2} →
  {A : Type u_5} →
    [inst : NonUnitalCStarAlgebra A] →
      [inst_1 : Fintype n] → CStarMatrix n n A →ₙₐ[ℂ] (WithCStarModule A (n → A) →L[ℂ] WithCStarModule A (n → A))ᵐᵒᵖ
-- Mathlib.RingTheory.Valuation.Extension
_private.Mathlib.RingTheory.Valuation.Extension.0.Valuation.HasExtension.termL₀ : Lean.ParserDescr
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
/-- The odd components are the connected components of odd cardinality. This definition excludes
infinite components.  -/
SimpleGraph.oddComponents : {V : Type u} → (G : SimpleGraph V) → Set G.ConnectedComponent
-- Mathlib.Algebra.Homology.HomotopyCategory
HomotopyCategory.instHasZeroObject : ∀ {ι : Type u_2} (V : Type u) [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroObject V],
  CategoryTheory.Limits.HasZeroObject (HomotopyCategory V c)
-- Mathlib.Data.Set.Lattice.Image
Set.seq_mono : ∀ {α : Type u_1} {β : Type u_2} {s₀ s₁ : Set (α → β)} {t₀ t₁ : Set α}, s₀ ⊆ s₁ → t₀ ⊆ t₁ → s₀.seq t₀ ⊆ s₁.seq t₁
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
ContinuousLinearMap.coe_domRestrict : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  {M₂ : Type u_5} [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] [inst_4 : Module R₁ M₁]
  [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂)
  (p : Submodule R₁ M₁), ⇑(f.domRestrict p) = (↑p).domRestrict ⇑f
-- Mathlib.Algebra.Module.SpanRank
Submodule.spanRank_eq_zero_iff_eq_bot : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {I : Submodule R M},
  I.spanRank = 0 ↔ I = ⊥
-- Mathlib.Topology.Instances.CantorSet
_private.Mathlib.Topology.Instances.CantorSet.0.preCantorSet.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- If `[]` approximates `f`, then `f = 0` eventually.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Approximates.elim_nil : ∀ {f basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis},
  (Tactic.ComputeAsymptotics.MultiseriesExpansion.mk Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil
        f).Approximates →
    f =ᶠ[Filter.atTop] 0
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry_replaceEntry_of_true : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α} {v : β k}
  (hl : Std.Internal.List.containsKey a (Std.Internal.List.replaceEntry k v l) = true),
  (k == a) = true → Std.Internal.List.getEntry a (Std.Internal.List.replaceEntry k v l) hl = ⟨k, v⟩
-- Mathlib.Combinatorics.SimpleGraph.Matching
/-- The subgraph `M` of `G` is a perfect matching on `G` if it's a matching and every vertex `G` is
matched.
 -/
SimpleGraph.Subgraph.IsPerfectMatching : {V : Type u_1} → {G : SimpleGraph V} → G.Subgraph → Prop
-- Mathlib.Analysis.Real.Cardinality
/-- The cardinality of the interval $(a, b]$.  -/
Cardinal.mk_Ioc_real : ∀ {a b : ℝ}, a < b → Cardinal.mk ↑(Set.Ioc a b) = Cardinal.continuum
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- For `x` not in `f`'s domain, `f.eval x` is consistent with `f`'s monotonicity.  -/
HahnEmbedding.Partial.eval_lt : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed)
  [inst_12 : IsOrderedAddMonoid R] [inst_13 : Archimedean R] {x : M},
  x ∉ (↑f).domain → ∀ (y : ↥(↑f).domain), x < ↑y → f.eval x < ↑↑f y
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Functor.FullyFaithful.homAddEquiv.eq_1 : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v, u_1} C]
  [inst_1 : CategoryTheory.CartesianMonoidalCategory C] [inst_2 : CategoryTheory.Category.{w, u_2} D]
  [inst_3 : CategoryTheory.CartesianMonoidalCategory D] {M X : C} [inst_4 : CategoryTheory.AddMonObj M]
  (F : CategoryTheory.Functor C D) [inst_5 : F.Monoidal] (hF : F.FullyFaithful),
  CategoryTheory.Functor.FullyFaithful.homAddEquiv F hF = { toEquiv := hF.homEquiv, map_add' := ⋯ }
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- Continuous bilinear map realizing `(f, z) ↦ f.smulRight z`.  -/
ContinuousMultilinearMap.smulRightL : (𝕜 : Type u) →
  {ι : Type v} →
    (E : ι → Type wE) →
      (G : Type wG) →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] →
            [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] →
              [inst_3 : SeminormedAddCommGroup G] →
                [inst_4 : NormedSpace 𝕜 G] →
                  [Fintype ι] → ContinuousMultilinearMap 𝕜 E 𝕜 →L[𝕜] G →L[𝕜] ContinuousMultilinearMap 𝕜 E G
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Subgroup.instHasDetPlusMinusOneFinOfNatNatRealOfIsArithmetic : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [h : Γ.IsArithmetic], Γ.HasDetPlusMinusOne
-- Mathlib.Data.Finset.Basic
Finset.union_erase_of_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a : α}, a ∈ s → ∀ (t : Finset α), s ∪ t.erase a = s ∪ t
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.substAlgHom.congr_simp : ∀ {R : Type u_2} [inst : CommRing R] {τ : Type u_3} {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {a a_1 : MvPowerSeries τ S} (e_a : a = a_1) (ha : PowerSeries.HasSubst a),
  PowerSeries.substAlgHom ha = PowerSeries.substAlgHom ⋯
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVPred.bin.inj : ∀ {w : ℕ} {lhs : Std.Tactic.BVDecide.BVExpr w} {op : Std.Tactic.BVDecide.BVBinPred} {rhs : Std.Tactic.BVDecide.BVExpr w}
  {w_1 : ℕ} {lhs_1 : Std.Tactic.BVDecide.BVExpr w_1} {op_1 : Std.Tactic.BVDecide.BVBinPred}
  {rhs_1 : Std.Tactic.BVDecide.BVExpr w_1},
  Std.Tactic.BVDecide.BVPred.bin lhs op rhs = Std.Tactic.BVDecide.BVPred.bin lhs_1 op_1 rhs_1 →
    w = w_1 ∧ lhs ≍ lhs_1 ∧ op = op_1 ∧ rhs ≍ rhs_1
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.typeToCat_obj : ∀ (X : Type u), CategoryTheory.typeToCat.obj X = CategoryTheory.Cat.of (CategoryTheory.Discrete X)
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
Nat.max_log_padicValNat_succ_eq_log_succ : ∀ {p : ℕ} (n : ℕ) [hp : Fact (Nat.Prime p)], max (Nat.log p n) (padicValNat p (n + 1)) = Nat.log p (n + 1)
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- Whiskering a 1-morphism is a functor.  -/
CategoryTheory.Bicategory.RightLift.whiskering : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} →
        {g : c ⟶ a} →
          {x : B} →
            (h : x ⟶ c) →
              CategoryTheory.Functor (CategoryTheory.Bicategory.RightLift f g)
                (CategoryTheory.Bicategory.RightLift f (CategoryTheory.CategoryStruct.comp h g))
-- Init.Data.List.Attach
List.mem_attachWith : ∀ {α : Type u_1} {l : List α} {q : α → Prop} (H : ∀ x ∈ l, q x) (x : { x // q x }), x ∈ l.attachWith q H ↔ ↑x ∈ l
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
AddEquiv.withBotCongr.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Add α] [inst_1 : Add β] (e : α ≃+ β),
  e.withBotCongr = { toEquiv := e.withBotCongr, map_add' := ⋯ }
-- Mathlib.Data.Fin.SuccPred
Fin.succ_ne_last_iff : ∀ {n : ℕ} (a : Fin (n + 1)), a.succ ≠ Fin.last (n + 1) ↔ a ≠ Fin.last n
-- Mathlib.Data.ZMod.Basic
ZMod.ringEquivOfPrime_eq_ringEquiv : ∀ (R : Type u_1) [inst : Ring R] [inst_1 : Fintype R] {p : ℕ} [inst_2 : CharP R p] (hp : Nat.Prime p)
  (hR : Fintype.card R = p), ZMod.ringEquivOfPrime R hp hR = ZMod.ringEquiv R hR
-- Init.Data.UInt.Basic
instModUInt32 : Mod UInt32
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule
PresheafOfModules.Submodule.top_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M : PresheafOfModules R} (X : Cᵒᵖ), ⊤.obj X = ⊤ X
-- Mathlib.CategoryTheory.Sites.Precoverage
/-- The collection of covering presieves for an object `X`.  -/
CategoryTheory.Precoverage.coverings : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.Precoverage C → (X : C) → Set (CategoryTheory.Presieve X)
-- Init.Meta.Defs
Lean.evalOptPrio : Option (Lean.TSyntax `prio) → Lean.MacroM ℕ
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
CategoryTheory.Limits.IsInitial.isIso_to : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] {I : C}
  (hI : CategoryTheory.Limits.IsInitial I) {A : C} (f : A ⟶ I), CategoryTheory.IsIso f
-- Mathlib.Order.Hom.WithTopBot
WithTop.toDualBotEquiv_symm_coe : ∀ {α : Type u_1} [inst : LE α] (a : α), WithTop.toDualBotEquiv.symm (OrderDual.toDual ↑a) = ↑(OrderDual.toDual a)
-- Mathlib.GroupTheory.IsSubnormal
Subgroup.subgroupOf.hcongr_4 : ∀ (G G' : Type u_1),
  G = G' →
    ∀ (inst : Group G) (inst' : Group G'),
      inst ≍ inst' →
        ∀ (H : Subgroup G) (H' : Subgroup G'),
          H ≍ H' → ∀ (K : Subgroup G) (K' : Subgroup G'), K ≍ K' → H.subgroupOf K ≍ H'.subgroupOf K'
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S}
  (h : CategoryTheory.Limits.ChosenPullback f₁ f₂) {Y : C} {f g : Y ⟶ h.pullback},
  CategoryTheory.CategoryStruct.comp f h.p₁ = CategoryTheory.CategoryStruct.comp g h.p₁ →
    CategoryTheory.CategoryStruct.comp f h.p₂ = CategoryTheory.CategoryStruct.comp g h.p₂ → f = g
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- Eta-expanded form of `MeasureTheory.AEStronglyMeasurable.pow` -/
MeasureTheory.AEStronglyMeasurable.fun_pow : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [inst_1 : Monoid β] [ContinuousMul β],
  MeasureTheory.AEStronglyMeasurable f μ → ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (fun i => f i ^ n) μ
-- Mathlib.RingTheory.Ideal.Maps
/-- If `f : R ≃+* S` is a ring isomorphism and `I : Ideal R`, then `comap f.symm I = map f I`.  -/
Ideal.comap_symm : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {I : Ideal R} (f : R ≃+* S),
  Ideal.comap f.symm I = Ideal.map f I
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.IrreducibleCloseds.isClosed' : ∀ {α : Type u_4} [inst : TopologicalSpace α] (self : TopologicalSpace.IrreducibleCloseds α), IsClosed self.carrier
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
CategoryTheory.Functor.instPreservesFiniteEffectiveEpiFamiliesOfPreservesEffectiveEpiFamilies : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) [F.PreservesEffectiveEpiFamilies],
  F.PreservesFiniteEffectiveEpiFamilies
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.monomial_def : ∀ {R : Type u_1} (n : ℕ) [inst : Semiring R] (a : R),
  (SkewPolynomial.monomial n) a = SkewMonoidAlgebra.single (Multiplicative.ofAdd n) a
-- Init.Data.Fin.Lemmas
Fin.castLE_castLE : ∀ {k m n : ℕ} (km : k ≤ m) (mn : m ≤ n) (i : Fin k), Fin.castLE mn (Fin.castLE km i) = Fin.castLE ⋯ i
-- Mathlib.Topology.NhdsSet
IsClosed.nhdsSet_le_sup : ∀ {X : Type u_2} [inst : TopologicalSpace X] (s : Set X) {t : Set X},
  IsClosed t → nhdsSet s ≤ nhdsSet (s ∩ t) ⊔ Filter.principal tᶜ
-- Mathlib.Topology.Order.ScottTopology
Topology.WithScott.instTopologicalSpace : {α : Type u_1} → [Preorder α] → TopologicalSpace (Topology.WithScott α)
-- Mathlib.Order.PartialSups
/-- Version of `ciSup_partialSups_eq` without boundedness assumptions, but requiring a
`ConditionallyCompleteLinearOrder` rather than just a `ConditionallyCompleteLattice`.  -/
ciSup_partialSups_eq' : ∀ {α : Type u_1} {ι : Type u_3} [inst : Preorder ι] [inst_1 : LocallyFiniteOrderBot ι]
  [inst_2 : ConditionallyCompleteLinearOrder α] (f : ι → α), ⨆ i, (partialSups f) i = ⨆ i, f i
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.isHashSelf_replaceₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α β),
  Std.DHashMap.Internal.Raw.WFImp ↑m → ∀ (a : α) (b : β a), Std.DHashMap.Internal.IsHashSelf (↑(m.replaceₘ a b)).buckets
-- Init.Data.Int.Gcd
Int.lcm_one : ∀ {a : ℤ}, a.lcm 1 = a.natAbs
-- Mathlib.Topology.Compactness.Lindelof
isLindelof_univ : ∀ {X : Type u} [inst : TopologicalSpace X] [h : LindelofSpace X], IsLindelof Set.univ
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.bifunctorComp₂₃Iso_inv_app_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {C₂₃ : Type u_5} {E : Type u_9}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃] [inst_3 : CategoryTheory.Category.{v_5, u_5} C₂₃]
  [inst_4 : CategoryTheory.Category.{v_9, u_9} E] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ E))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) (X : C₁) (X_1 : C₂) (X_2 : C₃),
  (((F.bifunctorComp₂₃Iso G₂₃).inv.app X).app X_1).app X_2 =
    CategoryTheory.CategoryStruct.id ((F.obj X).obj ((G₂₃.obj X_1).obj X_2))
-- Mathlib.Tactic.CategoryTheory.Reassoc
/-- Registers a handler for `reassocExpr`. The handler takes a proof of an equation
and returns a proof of the reassociation lemma.
Handlers are considered in order of registration.
They are applied directly to the equation in the body of the forall.
 -/
Mathlib.Tactic.Reassoc.registerReassocExpr : (Lean.Expr → Lean.MetaM (Lean.Expr × Array Lean.MVarId)) → IO Unit
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.inj_sigmaOfIsColimit_f_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) (i : E.I₀) (r : PUnit.{w + 1}) {Z : C}
  (h : S ⟶ Z),
  CategoryTheory.CategoryStruct.comp (c.inj i) (CategoryTheory.CategoryStruct.comp ((E.sigmaOfIsColimit hc).f r) h) =
    CategoryTheory.CategoryStruct.comp (E.f i) h
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.degree_of_subsingleton : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} [Subsingleton R], p.degree = ⊥
-- Mathlib.Topology.Order.Compact
instCompactIccSpaceProd : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : TopologicalSpace α] [CompactIccSpace α]
  [inst_3 : Preorder β] [inst_4 : TopologicalSpace β] [CompactIccSpace β], CompactIccSpace (α × β)
-- Mathlib.Analysis.Calculus.FDeriv.Basic
hasFDerivAtFilter_iff_tendsto : ∀ {𝕜 : 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}
  {f' : E →L[𝕜] F} {L : Filter (E × E)},
  HasFDerivAtFilter f f' L ↔ Filter.Tendsto (fun p => ‖p.1 - p.2‖⁻¹ * ‖f p.1 - f p.2 - f' (p.1 - p.2)‖) L (nhds 0)
-- Mathlib.Data.Part
Part.append_mem_append : ∀ {α : Type u_1} [inst : Append α] (a b : Part α) (ma mb : α), ma ∈ a → mb ∈ b → ma ++ mb ∈ a ++ b
-- Mathlib.Data.Matrix.Basis
Matrix.mul_single_apply_of_ne : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_7} [inst : DecidableEq m] [inst_1 : DecidableEq n]
  [inst_2 : Fintype m] [inst_3 : NonUnitalNonAssocSemiring α] (c : α) (i : m) (j : n) (a : l) (b : n),
  b ≠ j → ∀ (M : Matrix l m α), (M * Matrix.single i j c) a b = 0
-- Mathlib.Topology.Algebra.Group.SubmonoidClosure
closure_range_zsmul_eq_nsmul : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [CompactSpace G] [IsTopologicalAddGroup G] (x : G),
  closure (Set.range fun x_1 => x_1 • x) = closure (Set.range fun x_1 => x_1 • x)
-- Mathlib.Data.Nat.Factorial.Basic
Nat.factorial_inj : ∀ {m n : ℕ}, 1 < n → (n.factorial = m.factorial ↔ n = m)
-- Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
CategoryTheory.LocallyDiscrete.locallyDiscreteEquiv_apply : ∀ {C : Type u} (self : CategoryTheory.LocallyDiscrete C),
  CategoryTheory.LocallyDiscrete.locallyDiscreteEquiv self = self.as
-- Mathlib.Dynamics.Flow
/-- The forward orbit of a point under a flow `ϕ` is forward-invariant under `ϕ`.  -/
Flow.isForwardInvariant_forwardOrbit : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddMonoid τ]
  (ϕ : Flow τ α) [inst_3 : Preorder τ] [inst_4 : AddLeftMono τ] (x : α), IsForwardInvariant ϕ.toFun (ϕ.forwardOrbit x)
-- Mathlib.Data.Fin.SuccPred
Fin.succ_ne_last_of_lt : ∀ {n : ℕ} {p i : Fin n}, i < p → i.succ ≠ Fin.last n