mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get!_insertMany_list_of_not_mem_of_mem : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  [inst_4 : Inhabited α],
  m.WF →
    ∀ {l : List α} {k k' : α},
      (k == k') = true → k ∉ m → List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (m.insertMany l).get! k' = k
-- Mathlib.Algebra.Module.Submodule.Pointwise
/-- See also `Submodule.smul_iSup`.  -/
Submodule.smul_iSup' : ∀ {α : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Monoid α] [inst_4 : DistribMulAction α M] [inst_5 : SMulCommClass α R M] (a : α) {ι : Sort u_4}
  (f : ι → Submodule R M), a • ⨆ i, f i = ⨆ i, a • f i
-- Mathlib.Topology.List
List.continuous_cons : ∀ {α : Type u_1} [inst : TopologicalSpace α], Continuous fun x => x.1 :: x.2
-- Mathlib.GroupTheory.GroupAction.Embedding
Function.Embedding.smul_def : ∀ {G : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Group G] [inst_1 : MulAction G β] (g : G) (f : α ↪ β),
  g • f = f.trans (Equiv.toEmbedding (MulAction.toPerm g))
-- Mathlib.Algebra.GroupWithZero.Defs
NoZeroDivisors.mk : ∀ {M₀ : Type u_2} [inst : Mul M₀] [inst_1 : Zero M₀], (∀ {a b : M₀}, a * b = 0 → a = 0 ∨ b = 0) → NoZeroDivisors M₀
-- Mathlib.Topology.NhdsWithin
nhdsWithin_sUnion : ∀ {α : Type u_1} [inst : TopologicalSpace α] {S : Set (Set α)},
  S.Finite → ∀ (a : α), nhdsWithin a (⋃₀ S) = ⨆ s ∈ S, nhdsWithin a s
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.covers_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (J : CategoryTheory.GrothendieckTopology C)
  (S : CategoryTheory.Sieve X) (f : Y ⟶ X), J.Covers S f ↔ CategoryTheory.Sieve.pullback f S ∈ J Y
-- Std.Sat.CNF.Basic
Std.Sat.CNF.Internal.any_not_isEmpty_iff_exists_mem : ∀ {α : Type u_1} {f : Std.Sat.CNF α}, (f.clauses.any fun c => !List.isEmpty c) = true ↔ ∃ v, Std.Sat.CNF.VarMem v f
-- Mathlib.Tactic.CategoryTheory.Coherence
/-- **Alias** of `Mathlib.Tactic.Coherence.coherenceLoop`.

---

The main part of `coherence` tactic.  -/
Mathlib.Tactic.Coherence.coherence_loop : optParam ℕ 37 → Lean.Elab.Tactic.TacticM Unit
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.dropEndWhile_eq_self : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice}, s.endsWith pat = false → s.dropEndWhile pat = s
-- Mathlib.Tactic.CasesM
Lean.MVarId.casesType : Array Lean.Name → optParam Bool false → optParam Bool true → Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Init.Data.SInt.Lemmas
Int8.toInt16_lt : ∀ {a b : Int8}, a.toInt16 < b.toInt16 ↔ a < b
-- Mathlib.MeasureTheory.Function.AEEqOfIntegral
MeasureTheory.Integrable.ae_eq_zero_of_forall_setIntegral_eq_zero : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : α → E},
  MeasureTheory.Integrable f μ → (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0) → f =ᵐ[μ] 0
-- Mathlib.MeasureTheory.Covering.DensityTheorem
/-- A version of **Lebesgue differentiation theorem** for a sequence of closed balls whose
centers are not required to be fixed.  -/
IsUnifLocDoublingMeasure.ae_tendsto_average_norm_sub : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] (μ : MeasureTheory.Measure α)
  [IsUnifLocDoublingMeasure μ] [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ]
  {E : Type u_2} [inst_6 : NormedAddCommGroup E] {f : α → E},
  MeasureTheory.LocallyIntegrable f μ →
    ∀ (K : ℝ),
      ∀ᵐ (x : α) ∂μ,
        ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
          Filter.Tendsto δ l (nhdsWithin 0 (Set.Ioi 0)) →
            (∀ᶠ (j : ι) in l, x ∈ Metric.closedBall (w j) (K * δ j)) →
              Filter.Tendsto (fun j => ⨍ (y : α) in Metric.closedBall (w j) (δ j), ‖f y - f x‖ ∂μ) l (nhds 0)
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Cache.WF.below.push_cache : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α]
  {motive :
    (a : Array (Std.Sat.AIG.Decl α)) → (a_1 : Std.HashMap (Std.Sat.AIG.Decl α) ℕ) → Std.Sat.AIG.Cache.WF a a_1 → Prop}
  {decls : Array (Std.Sat.AIG.Decl α)} {cache : Std.HashMap (Std.Sat.AIG.Decl α) ℕ} {decl : Std.Sat.AIG.Decl α}
  (h : Std.Sat.AIG.Cache.WF decls cache),
  Std.Sat.AIG.Cache.WF.below h → motive decls cache h → Std.Sat.AIG.Cache.WF.below ⋯
-- Mathlib.Algebra.Algebra.Epi
TensorProduct.lid'_apply_tmul : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : Algebra.IsEpi R A] (M : Type u_3) [inst_4 : AddCommMonoid M] [inst_5 : Module R M] [inst_6 : Module A M]
  [inst_7 : IsScalarTower R A M] (a : A) (m : M), (TensorProduct.lid' R A M) (a ⊗ₜ[R] m) = a • m
-- Mathlib.Algebra.CharP.MixedCharZero
/-- In an `IsDomain R`, split any `Prop` over `R` into the three cases:
- *prime* characteristic.
- equal characteristic zero.
- mixed characteristic `(0, p)`.
 -/
split_by_characteristic_domain : ∀ (R : Type u_1) [inst : CommRing R] {P : Prop} [IsDomain R],
  (∀ (p : ℕ), Nat.Prime p → CharP R p → P) →
    (∀ (a : Algebra ℚ R), P) → (∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P) → P
-- Mathlib.Data.Finite.Sum
Finite.sum_left : ∀ {α : Type u_1} (β : Type u_3) [Finite (α ⊕ β)], Finite α
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.comp_apply : ∀ {R : Type u} {S : Type u₁} {T : Type u_1} [inst : Monoid R] [inst_1 : Monoid S] [inst_2 : Monoid T] {φ : R →* S}
  {A : Type v} {B : Type w} {C : Type w₁} [inst_3 : NonUnitalNonAssocSemiring A] [inst_4 : DistribMulAction R A]
  [inst_5 : NonUnitalNonAssocSemiring B] [inst_6 : DistribMulAction S B] [inst_7 : NonUnitalNonAssocSemiring C]
  [inst_8 : DistribMulAction T C] {ψ : S →* T} {χ : R →* T} (f : B →ₛₙₐ[ψ] C) (g : A →ₛₙₐ[φ] B)
  [inst_9 : φ.CompTriple ψ χ] (x : A), (f.comp g) x = f (g x)
-- Mathlib.Topology.ContinuousMap.SecondCountableSpace
/-- A version of `instSecondCountableTopology` with a technical assumption
instead of `[SecondCountableTopology X] [LocallyCompactSpace X]`.
It is here as a reminder of what could be an intermediate goal,
if someone tries to weaken the assumptions in the instance
(e.g., from `[LocallyCompactSpace X]` to `[LocallyCompactPair X Y]` - not sure if it's true).  -/
ContinuousMap.secondCountableTopology : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [SecondCountableTopology Y],
  (∃ S,
      S.Countable ∧
        (∀ K ∈ S, IsCompact K) ∧
          ∀ (f : C(X, Y)) (V : Set Y), IsOpen V → ∀ x ∈ ⇑f ⁻¹' V, ∃ K ∈ S, K ∈ nhds x ∧ Set.MapsTo (⇑f) K V) →
    SecondCountableTopology C(X, Y)
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.totalDegree_truncFinset : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {s : Finset (σ →₀ ℕ)} (p : MvPowerSeries σ R),
  ((MvPowerSeries.truncFinset R s) p).totalDegree ≤ s.sup ⇑Finsupp.degree
-- Mathlib.Geometry.Polygon.Basic
/-- A coercion to function so that vertices can
be written as `poly i` instead of `poly.vertices i`  -/
Polygon.instCoeFunForallFin : {P : Type u_3} → {n : ℕ} → CoeFun (Polygon P n) fun x => Fin n → P
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
/-- A limit (over a general filter) of measurable functions valued in a (pseudo) metrizable space is
measurable.  -/
measurable_of_tendsto_metrizable' : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace β]
  [TopologicalSpace.PseudoMetrizableSpace β] [inst_3 : MeasurableSpace β] [BorelSpace β] {ι : Type u_3} {f : ι → α → β}
  {g : α → β} (u : Filter ι) [u.NeBot] [u.IsCountablyGenerated],
  (∀ (i : ι), Measurable (f i)) → Filter.Tendsto f u (nhds g) → Measurable g
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.mul_add_right_left_iff : ∀ {R : Type u} [inst : CommRing R] {x y z : R}, IsCoprime (z * y + x) y ↔ IsCoprime x y
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.TacticFinishedSnapshot.mk.sizeOf_spec : ∀ (toSnapshot : Lean.Language.Snapshot) (state? : Option Lean.Elab.Tactic.SavedState)
  (moreSnaps : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)),
  sizeOf { toSnapshot := toSnapshot, state? := state?, moreSnaps := moreSnaps } =
    1 + sizeOf toSnapshot + sizeOf state? + sizeOf moreSnaps
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.Monad.comparison_obj_A : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) (X : D),
  ((CategoryTheory.Monad.comparison h).obj X).A = R.obj X
-- Mathlib.Data.Nat.Find
Nat.findGreatest_pos : ∀ {k : ℕ} {P : ℕ → Prop} [inst : DecidablePred P], 0 < Nat.findGreatest P k ↔ ∃ n, 0 < n ∧ n ≤ k ∧ P n
-- Mathlib.RingTheory.Noetherian.Basic
isNoetherian_map : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {P : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module S P] {σ : R →+* S}
  [inst_6 : RingHomSurjective σ] {s : Submodule R M} (f : M →ₛₗ[σ] P) [IsNoetherian R ↥s],
  IsNoetherian S ↥(Submodule.map f s)
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.ext : ∀ {X Y : AddMonCat} {f g : X ⟶ Y},
  (∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) → f = g
-- Std.Data.DHashMap.Raw
/-- Checks whether a key is present in a map, returning the associated value, and inserts a value for
the key if it was not found.

If the returned value is `some v`, then the returned map is unaltered. If it is `none`, then the
returned map has a new value inserted.

Equivalent to (but potentially faster than) calling `get?` followed by `insertIfNew`.

Uses the `LawfulBEq` instance to cast the retrieved value to the correct type.
 -/
Std.DHashMap.Raw.getThenInsertIfNew? : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] →
      [Hashable α] → [LawfulBEq α] → Std.DHashMap.Raw α β → (a : α) → β a → Option (β a) × Std.DHashMap.Raw α β
-- Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
/-- Any category with pullbacks and a terminal object has a limit cone for each walking pair.  -/
limitConeOfTerminalAndPullbacks : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasTerminal C] →
      [CategoryTheory.Limits.HasPullbacks C] →
        (F : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C) →
          CategoryTheory.Limits.LimitCone F
-- Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
CategoryTheory.LocallyDiscrete.instDecidableEq : {C : Type u} → [DecidableEq C] → DecidableEq (CategoryTheory.LocallyDiscrete C)
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
analyticOnNhd_sigmoid : AnalyticOnNhd ℝ Real.sigmoid Set.univ
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `IsAddTorsion.torsion_eq_top`.

---

The torsion additive submonoid of a torsion additive monoid is `⊤`.  -/
AddMonoid.IsTorsion.torsion_eq_top : ∀ {G : Type u_1} [inst : AddCommMonoid G], IsAddTorsion G → AddCommMonoid.addTorsion G = ⊤
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.bind₂.eq_1 : ∀ {σ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  (f : R →+* MvPolynomial σ S), MvPolynomial.bind₂ f = MvPolynomial.eval₂Hom f MvPolynomial.X
-- Init.Grind.AC
_private.Init.Grind.AC.0.Lean.Grind.AC.Seq.unionFuel.match_1.splitter : (motive : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Sort u_1) →
  (s₁ s₂ : Lean.Grind.AC.Seq) →
    ((x₁ x₂ : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.var x₁) (Lean.Grind.AC.Seq.var x₂)) →
      ((x₁ x : Lean.Grind.AC.Var) →
          (s : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.var x₁) (Lean.Grind.AC.Seq.cons x s)) →
        ((x : Lean.Grind.AC.Var) →
            (s : Lean.Grind.AC.Seq) →
              (x₂ : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.cons x s) (Lean.Grind.AC.Seq.var x₂)) →
          ((x₁ : Lean.Grind.AC.Var) →
              (s₁ : Lean.Grind.AC.Seq) →
                (x₂ : Lean.Grind.AC.Var) →
                  (s₂ : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.cons x₁ s₁) (Lean.Grind.AC.Seq.cons x₂ s₂)) →
            motive s₁ s₂
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteArchimedeanClass.liftOrderHom.eq_1 : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {α : Type u_2}
  [inst_3 : PartialOrder α] (f : { a // a ≠ 0 } → α)
  (h : ∀ (a b : { a // a ≠ 0 }), FiniteArchimedeanClass.mk ↑a ⋯ ≤ FiniteArchimedeanClass.mk ↑b ⋯ → f a ≤ f b),
  FiniteArchimedeanClass.liftOrderHom f h = { toFun := FiniteArchimedeanClass.lift f ⋯, monotone' := ⋯ }
-- Mathlib.RingTheory.SimpleModule.Isotypic
Submodule.MapSubtype.orderIso.eq_1 : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (p : Submodule R M),
  Submodule.MapSubtype.orderIso p =
    { toFun := fun p' => ⟨Submodule.map p.subtype p', ⋯⟩, invFun := fun q => Submodule.comap p.subtype ↑q,
      left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
-- Lean.Meta.Tactic.Grind.Ctor
/-- Heterogeneous case where constructor applications `a` and `b` have different types `α` and `β`.  -/
_private.Lean.Meta.Tactic.Grind.Ctor.0.Lean.Meta.Grind.propagateCtorHetero : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.weightedSMul_smul : ∀ {α : Type u_1} {F : Type u_3} {𝕜 : Type u_4} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F]
  {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst_2 : SMul 𝕜 F] [SMulCommClass ℝ 𝕜 F] (c : 𝕜) (s : Set α)
  (x : F), (MeasureTheory.weightedSMul μ s) (c • x) = c • (MeasureTheory.weightedSMul μ s) x
-- Lean.Data.Lsp.Basic
Lean.Lsp.TextDocumentIdentifier.mk : Lean.Lsp.DocumentUri → Lean.Lsp.TextDocumentIdentifier
-- Std.Http.Protocol.H1
/-- Applies an update function to the writer sub-state while preserving all other
machine fields.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.modifyWriter : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir →
    (Std.Http.Protocol.H1.Writer dir → Std.Http.Protocol.H1.Writer dir) → Std.Http.Protocol.H1.Machine dir
-- Init.System.IO
/-- The child process's standard error handle, if it was configured as `IO.Process.Stdio.piped`, or
`()` otherwise.
 -/
IO.Process.Child.stderr : {cfg : IO.Process.StdioConfig} → IO.Process.Child cfg → cfg.stderr.toHandleType
-- Mathlib.Geometry.Manifold.Algebra.Monoid
R_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {G : Type u_4}
  [inst_4 : Mul G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] (g h : G) [inst_7 : ContMDiffMul I (↑⊤) G],
  (smoothRightMul I g) h = h * g
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
/-- Given `i` and `j` in `Fin (n + 1)` such that `j ≠ i`, this is
the inclusion of `stdSimplex.face {j}ᶜ` in the horn `horn n i`.  -/
SSet.horn.faceι : {n : ℕ} → (i j : Fin (n + 1)) → j ≠ i → ((SSet.stdSimplex.face {j}ᶜ).toSSet ⟶ (SSet.horn n i).toSSet)
-- Mathlib.Analysis.Calculus.VectorField
/-- We have `[W, 0] = 0` for all vector fields `W`: this depends on the junk value 0
if `W` is not differentiable.  -/
VectorField.lieBracket_zero_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {W : E → E}, VectorField.lieBracket 𝕜 W 0 = 0
-- Mathlib.Analysis.Calculus.Deriv.AffineMap
AffineMap.hasDerivWithinAt_lineMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {a b : E} {s : Set 𝕜} {x : 𝕜}, HasDerivWithinAt (⇑(AffineMap.lineMap a b)) (b - a) s x
-- Mathlib.Topology.Algebra.Monoid.Defs
Filter.Tendsto.mul_const : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Mul M] [SeparatelyContinuousMul M] {α : Type u_2} {f : α → M}
  {x : Filter α} {a : M} (b : M), Filter.Tendsto f x (nhds a) → Filter.Tendsto (fun x => f x * b) x (nhds (a * b))
-- Mathlib.FieldTheory.Galois.Basic
/-- Let $F / K / k$ be a tower of field extensions. If $F$ is Galois over $k$,
then the normal closure of $K$ over $k$ in $F$ is Galois over $k$.  -/
IsGalois.normalClosure : ∀ (k : Type u_1) (K : Type u_2) (F : Type u_3) [inst : Field k] [inst_1 : Field K] [inst_2 : Field F]
  [inst_3 : Algebra k K] [inst_4 : Algebra k F] [IsGalois k F], IsGalois k ↥(IntermediateField.normalClosure k K F)
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.IsSymmetric.sub : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {φ ψ : MvPolynomial σ R},
  φ.IsSymmetric → ψ.IsSymmetric → (φ - ψ).IsSymmetric
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.type_fin : ∀ (n : ℕ), (Ordinal.type fun x1 x2 => x1 < x2) = ↑n
-- Std.Time.Format.Modifier
/-- `s`: Second of minute (e.g., 55).
 -/
Std.Time.Modifier.s : Std.Time.Number → Std.Time.Modifier
-- Aesop.Stats.File
Aesop.StatsFileRecord.syntax : Aesop.StatsFileRecord → String
-- Mathlib.Tactic.IntervalCases
/-- Given `e`, construct `(bound, n, p)` where `p` is a proof of `n ≤ e` or `n < e`
(characterized by `bound`), or `failure` if the type is not lower-bounded.  -/
Mathlib.Tactic.IntervalCases.Methods.initLB : Mathlib.Tactic.IntervalCases.Methods →
  Lean.Expr → Lean.MetaM (Mathlib.Tactic.IntervalCases.Bound × Lean.Expr × Lean.Expr)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic.0.termX_1 : Lean.ParserDescr
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
Real.smoothTransition.continuous : Continuous Real.smoothTransition
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.instIsOpenImmersionCommRingCatOfIsOpenImmersion : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) [AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f],
  AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f.toHom
-- Std.Sync.Channel
Std.instNonemptyCloseableChannel : ∀ {α : Type}, Nonempty (Std.CloseableChannel α)
-- Mathlib.Algebra.Group.WithOne.Defs
/-- Specialization of `Option.getD` to values in `WithOne α` that respects API boundaries.
 -/
WithOne.unoneD : {α : Type u} → α → WithOne α → α
-- Lean.Meta.Sym.SynthInstance
Lean.Meta.Sym.synthInstanceMeta? : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.addCommutator_le_map_addCommutator : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] {H₁ H₂ : AddSubgroup G} {f : G →+ G'}
  {K₁ K₂ : AddSubgroup G'},
  K₁ ≤ AddSubgroup.map f H₁ → K₂ ≤ AddSubgroup.map f H₂ → ⁅K₁, K₂⁆ ≤ AddSubgroup.map f ⁅H₁, H₂⁆
-- Mathlib.GroupTheory.GroupAction.DomAct.ActionHom
DomMulAct.instSMulCommClassDistribMulActionHomId : ∀ {M : Type u_1} {N : Type u_2} {A : Type u_3} {B : Type u_4} [inst : AddMonoid A] [inst_1 : DistribSMul M A]
  [inst_2 : Monoid N] [inst_3 : AddMonoid B] [inst_4 : DistribMulAction N A] [inst_5 : SMulCommClass M N A]
  [inst_6 : DistribMulAction N B] {M' : Type u_5} [inst_7 : DistribSMul M' A] [inst_8 : SMulCommClass M' N A]
  [SMulCommClass M M' A], SMulCommClass Mᵈᵐᵃ M'ᵈᵐᵃ (A →+[N] B)
-- Lean.Elab.DefView
Lean.Elab.DefView.binders : Lean.Elab.DefView → Lean.Syntax
-- Std.Http.Data.Body.Stream
/-- Resolved with `true` when consumed by a receiver, `false` when the channel closes.
 -/
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.Producer.done : Std.Http.Body.Channel.Producer✝ → IO.Promise Bool
-- Mathlib.Order.WithBot
WithTop.instPartialOrder : {α : Type u_1} → [PartialOrder α] → PartialOrder (WithTop α)
-- Mathlib.Algebra.Order.Interval.Basic
Interval.add_bot : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : Add α] [inst_2 : AddLeftMono α] [inst_3 : AddRightMono α]
  (s : Interval α), s + ⊥ = ⊥
-- Mathlib.Analysis.Matrix.Normed
Matrix.frobenius_normedStarGroup : ∀ {m : Type u_3} {α : Type u_5} [inst : Fintype m] [inst_1 : SeminormedAddCommGroup α] [inst_2 : StarAddMonoid α]
  [NormedStarGroup α], NormedStarGroup (Matrix m m α)
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- Locally path-connected spaces are locally connected.  -/
instLocallyConnectedSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyPathConnectedSpace X], LocallyConnectedSpace X
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.polyCharpoly_coeff_eval : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup L]
  [inst_2 : Module R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] (φ : L →ₗ[R] Module.End R M)
  [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] [inst_7 : Module.Free R M] [inst_8 : Module.Finite R M]
  (b : Module.Basis ι R L) (x : L) (i : ℕ),
  (MvPolynomial.eval ⇑(b.repr x)) ((φ.polyCharpoly b).coeff i) = (LinearMap.charpoly (φ x)).coeff i
-- Mathlib.Algebra.Order.Ring.Cone
Subsemiring.nonneg.congr_simp : ∀ (R : Type u_1) [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R],
  Subsemiring.nonneg R = Subsemiring.nonneg R
-- Mathlib.Data.Stream.Init
Stream'.append_eq_cons : ∀ {α : Type u} {a : α} {as : Stream' α}, [a] ++ₛ as = Stream'.cons a as
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α], m₁.WF → m₂.WF → ∀ {k : α} {fallback : β k}, k ∈ m₂ → (m₁ \ m₂).getD k fallback = fallback
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.wideCoequalizer.π_desc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)}
  [inst_1 : CategoryTheory.Limits.HasWideCoequalizer f] [inst_2 : Nonempty J] {W : C} (k : Y ⟶ W)
  (h : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) k = CategoryTheory.CategoryStruct.comp (f j₂) k),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideCoequalizer.π f)
      (CategoryTheory.Limits.wideCoequalizer.desc k h) =
    k
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_alter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] [Inhabited α] (h : t.WF) {k k' : α} {f : Option (β k) → Option (β k)}
  {hc : k' ∈ Std.DTreeMap.Internal.Impl.alter! k f t},
  (Std.DTreeMap.Internal.Impl.alter! k f t).getKey k' hc = if heq : compare k k' = Ordering.eq then k else t.getKey k' ⋯
-- Mathlib.Order.RelSeries
RelSeries.instInhabited : {α : Type u_1} → (r : SetRel α α) → [Inhabited α] → Inhabited (RelSeries r)
-- Lean.Meta.Tactic.Simp.Arith.Int.Simp
Lean.Meta.Simp.Arith.Int.simpLe? : Lean.Expr → Bool → Lean.MetaM (Option (Lean.Expr × Lean.Expr))
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxc.Iterator.step_eq_monadicStep : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α] {it : Std.Iter α},
  Std.Rxc.Iterator.step it = Std.IterStep.mapIterator Std.IterM.toIter (Std.Rxc.Iterator.Monadic.step it.toIterM)
-- Mathlib.MeasureTheory.Covering.Differentiation
/-- Given an arbitrary set `s`, then `μ (s ∩ a) / μ a` converges to `1` when `a` shrinks to a
typical point of `s` along a Vitali family. This shows that almost every point of `s` is a
Lebesgue density point for `s`. A stronger version for measurable sets is given
in `ae_tendsto_measure_inter_div_of_measurableSet`.  -/
VitaliFamily.ae_tendsto_measure_inter_div : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] (s : Set α),
  ∀ᵐ (x : α) ∂μ.restrict s, Filter.Tendsto (fun a => μ (s ∩ a) / μ a) (v.filterAt x) (nhds 1)
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charpoly_units_conj' : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : (Matrix n n R)ˣ)
  (N : Matrix n n R), ((↑M)⁻¹ * N * ↑M).charpoly = N.charpoly