mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting.0.CategoryTheory.Limits.termG₁_1 : Lean.ParserDescr
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryExtensive C],
  CategoryTheory.FinitaryPreExtensive C
-- Mathlib.Logic.Equiv.Fintype
Function.Embedding.toEquivRange_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq β] (f : α ↪ β) (a : α),
  f.toEquivRange a = ⟨f a, ⋯⟩
-- Mathlib.Data.Finset.Sups
Finset.diffs_right_comm : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] (s t u : Finset α),
  (s.diffs t).diffs u = (s.diffs u).diffs t
-- Mathlib.Data.Prod.Basic
Function.Involutive.prodMap : ∀ {α : Type u_1} {β : Type u_2} {f : α → α} {g : β → β},
  Function.Involutive f → Function.Involutive g → Function.Involutive (Prod.map f g)
-- Mathlib.Tactic.FunProp.FunctionData
Mathlib.Meta.FunProp.MorApplication.noConfusionType : Sort v✝ → Mathlib.Meta.FunProp.MorApplication → Mathlib.Meta.FunProp.MorApplication → Sort v✝
-- Mathlib.Topology.Order.IsLUB
exists_seq_strictAnti_tendsto_nhdsWithin : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [NoMaxOrder α] [FirstCountableTopology α] (x : α),
  ∃ u, StrictAnti u ∧ (∀ (n : ℕ), x < u n) ∧ Filter.Tendsto u Filter.atTop (nhdsWithin x (Set.Ioi x))
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.span_top : ∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] (b : Module.Basis ι K E), Submodule.span K ↑(Submodule.span ℤ (Set.range ⇑b)) = ⊤
-- Mathlib.Topology.UniformSpace.UniformEmbedding
/-- Sets of a subtype are complete iff their image under the coercion is complete.  -/
Subtype.isComplete_iff : ∀ {α : Type u} [inst : UniformSpace α] {p : α → Prop} {s : Set { x // p x }},
  IsComplete s ↔ IsComplete (Subtype.val '' s)
-- Init.Data.Int.Linear
Int.Internal.Linear.le_of_le_cert.eq_def : ∀ (p₁ p₂ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.le_of_le_cert p₁ p₂ =
    match p₁, p₂ with
    | Int.Internal.Linear.Poly.add k v p, Int.Internal.Linear.Poly.num k_1 => false
    | Int.Internal.Linear.Poly.num k, Int.Internal.Linear.Poly.add k_1 v p => false
    | Int.Internal.Linear.Poly.num c₁, Int.Internal.Linear.Poly.num c₂ => decide (c₁ ≥ c₂)
    | Int.Internal.Linear.Poly.add a₁ x₁ p₁, Int.Internal.Linear.Poly.add a₂ x₂ p₂ =>
      a₁ == a₂ && x₁ == x₂ && Int.Internal.Linear.le_of_le_cert p₁ p₂
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.eval₂Hom.congr_simp : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : UniformSpace R] {S : Type u_3} [inst_2 : CommRing S]
  [inst_3 : UniformSpace S] {φ φ_1 : R →+* S} (e_φ : φ = φ_1) {a a_1 : σ → S} (e_a : a = a_1)
  [inst_4 : IsTopologicalSemiring R] [inst_5 : IsUniformAddGroup R] [inst_6 : IsUniformAddGroup S]
  [inst_7 : CompleteSpace S] [inst_8 : T2Space S] [inst_9 : IsTopologicalRing S] [inst_10 : IsLinearTopology S S]
  (hφ : Continuous ⇑φ) (ha : MvPowerSeries.HasEval a), MvPowerSeries.eval₂Hom hφ ha = MvPowerSeries.eval₂Hom ⋯ ⋯
-- Mathlib.Order.Minimal
minimal_false : ∀ {α : Type u_2} {x : α} [inst : LE α], ¬Minimal (fun x => False) x
-- Mathlib.RingTheory.Congruence.Defs
RingCon.nsmul : ∀ {S : Type u_2} [inst : AddMonoid S] [inst_1 : Mul S] (t : RingCon S) (m : ℕ) {x y : S}, t x y → t (m • x) (m • y)
-- Mathlib.MeasureTheory.Covering.VitaliFamily
VitaliFamily.FineSubfamilyOn.measure_le_tsum : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  {v : VitaliFamily μ} {f : X → Set (Set X)} {s : Set X} (h : v.FineSubfamilyOn f s) [SecondCountableTopology X],
  μ s ≤ ∑' (x : ↑h.index), μ (h.covering ↑x)
-- Mathlib.Order.Minimal
Minimal.eq_of_superset : ∀ {α : Type u_2} {P : Set α → Prop} {s t : Set α}, Minimal P s → P t → t ⊆ s → s = t
-- Mathlib.Algebra.Category.CoalgCat.Basic
CoalgCat.moduleCat_of_toModuleCat : ∀ {R : Type u} [inst : CommRing R] (X : CoalgCat R), ModuleCat.of R ↑X.toModuleCat = X.toModuleCat
-- Init.Data.SInt.Lemmas
Int8.lt_iff_le_and_ne : ∀ {a b : Int8}, a < b ↔ a ≤ b ∧ a ≠ b
-- Mathlib.LinearAlgebra.Dual.BaseChange
IsBaseChange.toDual.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] {V : Type u_2} [inst_1 : AddCommMonoid V] [inst_2 : Module R V] {W : Type u_3}
  [inst_3 : AddCommMonoid W] [inst_4 : Module R W] {A : Type u_4} [inst_5 : CommSemiring A] [inst_6 : Algebra R A]
  [inst_7 : Module A W] [inst_8 : IsScalarTower R A W] {j j_1 : V →ₗ[R] W} (e_j : j = j_1) (ibc : IsBaseChange A j),
  ibc.toDual = ⋯.toDual
-- Init.Data.BitVec.Lemmas
BitVec.toInt_intMin_le : ∀ {w : ℕ} (x : BitVec w), (BitVec.intMin w).toInt ≤ x.toInt
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.ofNormedAddCommGroup.congr_simp : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β] (f f_1 : α → β)
  (e_f : f = f_1) (Hf : Continuous f) (C C_1 : ℝ) (e_C : C = C_1) (H : ∀ (x : α), ‖f x‖ ≤ C),
  BoundedContinuousFunction.ofNormedAddCommGroup f Hf C H = BoundedContinuousFunction.ofNormedAddCommGroup f_1 ⋯ C_1 ⋯
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.instZero : {R : Type uR} →
  {ι : Type uι} →
    {M₁ : ι → Type v₁} →
      {M₂ : Type v₂} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] → [inst_4 : Module R M₂] → Zero (MultilinearMap R M₁ M₂)
-- Init.Data.String.Lemmas.Pattern.Basic
/-- Predicate stating that the region between the start of the slice `s` and the position
`endPos` matches the pattern `pat`. Note that there might be a longer match, see
`String.Slice.Pattern.IsLongestMatch`.
 -/
String.Slice.Pattern.Model.IsMatch : {ρ : Type} → (pat : ρ) → [String.Slice.Pattern.Model.PatternModel pat] → {s : String.Slice} → s.Pos → Prop
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
/-- Helper lemma for `integral_log`: case where `a = 0`.  -/
integral_log_from_zero : ∀ {b : ℝ}, ∫ (s : ℝ) in 0..b, Real.log s = b * Real.log b - b
-- Init.Data.Fin.Lemmas
Fin.rev_last : ∀ (n : ℕ), (Fin.last n).rev = 0
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The natural cocone over the forgetful functor `Over X ⥤ T` with cocone point `X`.  -/
CategoryTheory.Over.forgetCocone : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] → (X : T) → CategoryTheory.Limits.Cocone (CategoryTheory.Over.forget X)
-- Mathlib.Computability.RE
Nat.Partrec.merge' : ∀ {f g : ℕ →. ℕ},
  Nat.Partrec f →
    Nat.Partrec g → ∃ h, Nat.Partrec h ∧ ∀ (a : ℕ), (∀ x ∈ h a, x ∈ f a ∨ x ∈ g a) ∧ ((h a).Dom ↔ (f a).Dom ∨ (g a).Dom)
-- Mathlib.RingTheory.OreLocalization.Ring
OreLocalization.universalHom.congr_simp : ∀ {R : Type u_1} [inst : Semiring R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {T : Type u_3}
  [inst_2 : Semiring T] (f f_1 : R →+* T) (e_f : f = f_1) (fS fS_1 : ↥S →* Tˣ) (e_fS : fS = fS_1)
  (hf : ∀ (s : ↥S), f ↑s = ↑(fS s)), OreLocalization.universalHom f fS hf = OreLocalization.universalHom f_1 fS_1 ⋯
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.IsSymm.zpow : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  {A : Matrix n' n' R}, A.IsSymm → ∀ (k : ℤ), (A ^ k).IsSymm
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.evaln.eq_8 : ∀ (k : ℕ) (cf cg : Nat.Partrec.Code),
  Nat.Partrec.Code.evaln k.succ (cf.prec cg) = fun n => do
    guard (n ≤ k)
    Nat.unpaired
        (fun a n =>
          Nat.casesOn n (Nat.Partrec.Code.evaln (k + 1) cf a) fun y => do
            let i ← Nat.Partrec.Code.evaln k (cf.prec cg) (Nat.pair a y)
            Nat.Partrec.Code.evaln (k + 1) cg (Nat.pair a (Nat.pair y i)))
        n
-- Mathlib.Order.Max
/-- Order without maximal elements. Sometimes called cofinal.  -/
NoMaxOrder : (α : Type u_3) → [LT α] → Prop
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_le_size_insertMany_list : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {l : List ((a : α) × β a)}, t.size ≤ (↑(t.insertMany l ⋯)).size
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.mapOfCompatibleSMul_surjective : ∀ (R : Type u_1) [inst : CommSemiring R] (A : Type u_22) (S : Type u_23) (M : Type u_24) (N : Type u_25)
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N]
  [inst_5 : CommSemiring A] [inst_6 : Module A M] [inst_7 : Module A N] [inst_8 : SMulCommClass R A M]
  [inst_9 : CommSemiring S] [inst_10 : Module S M] [inst_11 : SMulCommClass R S M] [inst_12 : SMulCommClass A S M]
  [inst_13 : TensorProduct.CompatibleSMul R A M N], Function.Surjective ⇑(TensorProduct.mapOfCompatibleSMul R A S M N)
-- Mathlib.InformationTheory.KullbackLeibler.KLFun
InformationTheory.klFun_apply : ∀ (x : ℝ), InformationTheory.klFun x = x * Real.log x + 1 - x
-- Lean.Data.JsonRpc
Lean.JsonRpc.Response.result : {α : Type u} → Lean.JsonRpc.Response α → α
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.leftAdjointOfEquiv.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {G : CategoryTheory.Functor D C} {F_obj : C → D} (e e_1 : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y))
  (e_e : e = e_1)
  (he :
    ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y),
      (e X Y') (CategoryTheory.CategoryStruct.comp h g) = CategoryTheory.CategoryStruct.comp ((e X Y) h) (G.map g)),
  CategoryTheory.Adjunction.leftAdjointOfEquiv e he = CategoryTheory.Adjunction.leftAdjointOfEquiv e_1 ⋯
-- Mathlib.RingTheory.Noetherian.Basic
/-- Modules over the trivial ring are Noetherian.  -/
isNoetherian_of_subsingleton : ∀ (R : Type u_1) (M : Type u_2) [Subsingleton R] [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  IsNoetherian R M
-- Mathlib.Algebra.Module.Bimodule
Subbimodule.coe_toSubbimoduleInt : ∀ (R : Type u_1) (S : Type u_2) (M : Type u_3) [inst : Ring R] [inst_1 : Ring S] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : Module S M] [inst_5 : SMulCommClass R S M] (p : Submodule (TensorProduct ℕ R S) M),
  ↑(Subbimodule.toSubbimoduleInt R S M p) = ↑p
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- A charted space over a discrete space is discrete.  -/
ChartedSpace.discreteTopology : ∀ (H : Type u) (M : Type u_2) [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [ChartedSpace H M]
  [DiscreteTopology H], DiscreteTopology M
-- Mathlib.Topology.Connected.Basic
isConnected_univ_pi : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] {s : (i : ι) → Set (X i)},
  IsConnected (Set.univ.pi s) ↔ ∀ (i : ι), IsConnected (s i)
-- Mathlib.Topology.Perfect
preperfect_iff_nhds : ∀ {α : Type u_1} [inst : TopologicalSpace α] {C : Set α}, Preperfect C ↔ ∀ x ∈ C, ∀ U ∈ nhds x, ∃ y ∈ U ∩ C, y ≠ x
-- Std.Data.HashSet.Raw
/-- Checks if given key is contained and returns the key if it is, otherwise `fallback`.
If they key is contained the result is guaranteed to be pointer equal to the key in the set.
 -/
Std.HashSet.Raw.getD : {α : Type u} → [BEq α] → [Hashable α] → Std.HashSet.Raw α → α → α → α
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.norm_mkPiAlgebraFin_succ_le : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {n : ℕ} {A : Type u_1} [inst_1 : SeminormedRing A]
  [inst_2 : NormedAlgebra 𝕜 A], ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n.succ A‖ ≤ 1
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
QuadraticForm.tensorLId_apply : ∀ {R : Type uR} {M₂ : Type uM₂} [inst : CommRing R] [inst_1 : AddCommGroup M₂] [inst_2 : Module R M₂]
  [inst_3 : Invertible 2] (Q₂ : QuadraticForm R M₂) (x : TensorProduct R R M₂),
  Q₂.tensorLId x = (TensorProduct.lid R M₂) x
-- Init.Grind.Ring.Basic
Lean.Grind.Ring.intCast_sub : ∀ {α : Type u} [inst : Lean.Grind.Ring α] (x y : ℤ), ↑(x - y) = ↑x - ↑y
-- Plausible.Sampleable
Plausible.NoShrink.sampleableExt : {α : Type u_1} → [Plausible.SampleableExt α] → [Repr α] → Plausible.SampleableExt (Plausible.NoShrink α)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsDenseSubsite.isLocallyFaithful' : ∀ {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} (J : CategoryTheory.GrothendieckTopology C)
  {K : CategoryTheory.GrothendieckTopology D} {G : CategoryTheory.Functor C D}
  [self : CategoryTheory.Functor.IsDenseSubsite J K G], G.IsLocallyFaithful K
-- Mathlib.Algebra.Torsor.Defs
Equiv.coe_smulConst_symm : ∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [inst_1 : Torsor G P] (p : P),
  ⇑(Equiv.smulConst p).symm = fun p' => p' /ₛ p
-- Lean.Server.FileWorker.SignatureHelp
Lean.Server.FileWorker.SignatureHelp.Candidate.mk.injEq : ∀ (kind : Lean.Server.FileWorker.SignatureHelp.CandidateKind) (appStx : Lean.Syntax)
  (kind_1 : Lean.Server.FileWorker.SignatureHelp.CandidateKind) (appStx_1 : Lean.Syntax),
  ({ kind := kind, appStx := appStx } = { kind := kind_1, appStx := appStx_1 }) = (kind = kind_1 ∧ appStx = appStx_1)
-- Init.Notation
/-- This attribute marks a code action that triggers on specific commands.

* `@[command_code_action kind]`: This is a code action which applies to applications of the command
`kind` (a command syntax kind), which can replace the command or insert things before or after it.

* `@[command_code_action kind₁ kind₂]`: shorthand for
`@[command_code_action kind₁, command_code_action kind₂]`.

* `@[command_code_action]`: This is a command code action that applies to all commands.
Use sparingly.
 -/
Lean.command_code_action : Lean.ParserDescr
-- Mathlib.Algebra.Free
FreeSemigroup.mul_seq : ∀ {α β : Type u} {f g : FreeSemigroup (α → β)} {x : FreeSemigroup α}, f * g <*> x = (f <*> x) * (g <*> x)
-- Mathlib.NumberTheory.Multiplicity
dvd_geom_sum₂_iff_of_dvd_sub' : ∀ {R : Type u_1} {n : ℕ} [inst : CommRing R] {x y p : R},
  p ∣ x - y → (p ∣ ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) ↔ p ∣ ↑n * x ^ (n - 1))
-- Mathlib.Tactic.GCongr.Core
/-- Add an unsolved goal to the `newGoals` array in the state.  -/
Mathlib.Tactic.GCongr.pushNewGoal : Lean.MVarId → Mathlib.Tactic.GCongr.GCongrM Unit
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.mk.congr_simp : ∀ {numVarsSucc : ℕ} (clause clause_1 : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin numVarsSucc))
  (e_clause : clause = clause_1)
  (nodupkey : ∀ (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin numVarsSucc), (l, true) ∉ clause ∨ (l, false) ∉ clause)
  (nodup : List.Nodup clause),
  { clause := clause, nodupkey := nodupkey, nodup := nodup } = { clause := clause_1, nodupkey := ⋯, nodup := ⋯ }
-- Mathlib.GroupTheory.SpecificGroups.ZGroup
/-- A finite Z-group has cyclic abelianization.  -/
IsZGroup.isCyclic_abelianization : ∀ {G : Type u_1} [inst : Group G] [Finite G] [IsZGroup G], IsCyclic (Abelianization G)
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.IsHomogeneous.coeff_eq_zero : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {φ : MvPolynomial σ R} {n : ℕ},
  φ.IsHomogeneous n → ∀ {d : σ →₀ ℕ}, Finsupp.degree d ≠ n → MvPolynomial.coeff d φ = 0
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csInf_lt_iff : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} {a : α},
  BddBelow s → s.Nonempty → (sInf s < a ↔ ∃ b ∈ s, b < a)
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
Ordinal.CNF.eval_single_add : ∀ (b : Ordinal.{u_1}) {e x : Ordinal.{u_1}} {f : Ordinal.{u_1} →₀ Ordinal.{u_1}},
  (∀ e' ∈ f.support, e' ≤ e) → Ordinal.CNF.eval b ((fun₀ | e => x) + f) = b ^ e * x + Ordinal.CNF.eval b f
-- Mathlib.Algebra.Symmetrized
SymAlg.instZero : {α : Type u_1} → [Zero α] → Zero αˢʸᵐ
-- Mathlib.Data.Int.ModEq
/-- Cancel right multiplication on both sides of the `≡` and in the modulus.

For cancelling right multiplication in the modulus, see `Int.ModEq.of_mul_right`.  -/
Int.ModEq.mul_right_cancel' : ∀ {m a b c : ℤ}, c ≠ 0 → a * c ≡ b * c [ZMOD m * c] → a ≡ b [ZMOD m]
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.tmul_ite : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (x₁ : M) (x₂ : N) (P : Prop)
  [inst_5 : Decidable P], (x₁ ⊗ₜ[R] if P then x₂ else 0) = if P then x₁ ⊗ₜ[R] x₂ else 0
-- Lean.Language.Lean.Types
Lean.Language.Lean.instNonemptyCommandParsedSnapshot : Nonempty Lean.Language.Lean.CommandParsedSnapshot
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.brecOn.eq : ∀ {V : Type u} {G : SimpleGraph V} {motive : (a a_1 : V) → G.Walk a a_1 → Sort u_1} {a a_1 : V} (t : G.Walk a a_1)
  (F_1 : (a a_2 : V) → (t : G.Walk a a_2) → SimpleGraph.Walk.below t → motive a a_2 t),
  SimpleGraph.Walk.brecOn t F_1 = F_1 a a_1 t (SimpleGraph.Walk.brecOn.go t F_1).2
-- Mathlib.Topology.Algebra.OpenSubgroup
/-- The type of open subgroups of a topological additive group.  -/
OpenAddSubgroup : (G : Type u_1) → [AddGroup G] → [TopologicalSpace G] → Type u_1
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i_assoc_apply : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) {Z : ModuleCat R} (h : S.X₂ ⟶ Z)
  (x : ↑S.cycles),
  (CategoryTheory.ConcreteCategory.hom h)
      ((CategoryTheory.ConcreteCategory.hom S.moduleCatLeftHomologyData.i)
        ((CategoryTheory.ConcreteCategory.hom S.moduleCatCyclesIso.hom) x)) =
    (CategoryTheory.ConcreteCategory.hom h) ((CategoryTheory.ConcreteCategory.hom S.iCycles) x)
-- Mathlib.Algebra.Group.Subgroup.Order
Subsemigroup.strictMono_topEquiv : ∀ {G : Type u_1} [inst : CommMonoid G] [inst_1 : Preorder G], StrictMono ⇑Subsemigroup.topEquiv
-- Init.Data.Option.Lemmas
Option.all_min : ∀ {α : Type u_1} [inst : Min α] {o o' : Option α} {p : α → Bool},
  (∀ (a b : α), p (a ⊓ b) = (p a || p b)) → Option.all p (o ⊓ o') = (Option.all p o || Option.all p o')
-- Lean.Elab.SyntheticMVars
/-- Used to implement `synthesizeUsingDefault`. This method only consider default instances with the given priority.  -/
_private.Lean.Elab.SyntheticMVars.0.Lean.Elab.Term.synthesizeSomeUsingDefaultPrio : ℕ → Lean.Elab.TermElabM Bool
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.map_span : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (s : Set P₁),
  AffineSubspace.map f (affineSpan k s) = affineSpan k (⇑f '' s)
-- Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
AlgebraicGeometry.SurjectiveOnStalks.mk : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  (∀ (x : ↥X), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x))) →
    AlgebraicGeometry.SurjectiveOnStalks f
-- Mathlib.Order.Monotone.Basic
Nat.rel_of_forall_rel_succ_of_le_of_le : ∀ {β : Type v} (r : β → β → Prop) [Std.Refl r] [IsTrans β r] {f : ℕ → β} {a : ℕ},
  (∀ (n : ℕ), a ≤ n → r (f n) (f (n + 1))) → ∀ ⦃b c : ℕ⦄, a ≤ b → b ≤ c → r (f b) (f c)
-- Init.Data.UInt.Lemmas
UInt64.toBitVec_toUInt32 : ∀ (n : UInt64), n.toUInt32.toBitVec = BitVec.setWidth 32 n.toBitVec
-- Mathlib.Data.Finite.Defs
Equiv.set_finite_iff : ∀ {α : Type u} {β : Type v} {s : Set α} {t : Set β} (hst : ↑s ≃ ↑t), s.Finite ↔ t.Finite
-- Mathlib.Order.CompleteLattice.PiLex
Pi.Lex.le_sSup_apply : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → CompleteLinearOrder (α i)]
  [inst_2 : WellFoundedLT ι] {s : Set (Lex ((i : ι) → (fun i => α i) i))} {i : ι}
  {e : Lex ((i : ι) → (fun i => α i) i)}, e ∈ s → (∀ j < i, e j = sSup s j) → e i ≤ sSup s i
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.denote_blastShiftConcat : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α)
  (target : Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.ShiftConcatInput aig w) (assign : α → Bool) (idx : ℕ)
  (hidx : idx < w),
  ⟦assign,
      { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastShiftConcat aig target).aig,
        ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastShiftConcat aig target).vec.get idx hidx }⟧ =
    if idx = 0 then ⟦assign, { aig := aig, ref := target.bit }⟧
    else ⟦assign, { aig := aig, ref := target.lhs.get (idx - 1) ⋯ }⟧
-- Mathlib.RingTheory.Perfection
Perfection.coeff_symm_frobeniusEquiv : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [inst_1 : CharP R p] (f : Perfection R p)
  (n : ℕ), (Perfection.coeff R p n) ((frobeniusEquiv (Perfection R p) p).symm f) = (Perfection.coeff R p (n + 1)) f
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
/-- A category with fibrations is a category equipped with
a class of morphisms named "fibrations".  -/
HomotopicalAlgebra.CategoryWithFibrations : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max u v)
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.isUniformInducing_postcomp : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂]
  [inst_2 : NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [inst_3 : RingHomCompTriple σ τ ρ]
  {E : Type u_4} {F : Type u_5} {G : Type u_6} [inst_4 : AddCommGroup E] [inst_5 : Module 𝕜₁ E]
  [inst_6 : AddCommGroup F] [inst_7 : Module 𝕜₂ F] [inst_8 : AddCommGroup G] [inst_9 : Module 𝕜₃ G]
  [inst_10 : TopologicalSpace E] [inst_11 : UniformSpace F] [inst_12 : IsUniformAddGroup F] [inst_13 : UniformSpace G]
  [inst_14 : IsUniformAddGroup G] (f : F →SL[τ] G), IsUniformInducing ⇑f → IsUniformInducing f.comp
-- Mathlib.Logic.Function.Basic
Function.Injective.of_comp_right : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : γ → α},
  Function.Injective (f ∘ g) → Function.Surjective g → Function.Injective f
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
IsUnit.aestronglyMeasurable_const_smul_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} {M : Type u_5} [inst_1 : Monoid M] [inst_2 : MulAction M β] [ContinuousConstSMul M β] {c : M},
  IsUnit c → (MeasureTheory.AEStronglyMeasurable (fun x => c • f x) μ ↔ MeasureTheory.AEStronglyMeasurable f μ)
-- Mathlib.CategoryTheory.MorphismProperty.LocalEpi
CategoryTheory.ObjectProperty.localEpi_isoClosure : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C},
  P.isoClosure.localEpi = P.localEpi