mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Matrix.Diagonal
Matrix.transpose_eq_natCast : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : AddMonoidWithOne α] {M : Matrix n n α} {d : ℕ},
  M.transpose = ↑d ↔ M = ↑d
-- Lean.Elab.Do.Basic
Lean.Elab.Do.ContInfo.toContInfoRef : Lean.Elab.Do.ContInfo → Lean.Elab.Do.ContInfoRef
-- Mathlib.Algebra.Group.Defs
left_neg_eq_right_neg : ∀ {M : Type u_2} [inst : AddMonoid M] {a b c : M}, b + a = 0 → a + c = 0 → b = c
-- Mathlib.Tactic.Ring.Basic
Mathlib.Tactic.Ring.of_eq : ∀ {α : Sort u_2} {a b c : α}, a = c → b = c → a = b
-- Mathlib.RingTheory.Smooth.Kaehler
derivationOfSectionOfKerSqZero_apply_coe : ∀ {R : Type u_1} {P : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing P] [inst_2 : CommRing S]
  [inst_3 : Algebra R P] [inst_4 : Algebra R S] (f : P →ₐ[R] S) (hf' : RingHom.ker f ^ 2 = ⊥) (g : S →ₐ[R] P)
  (hg : f.comp g = AlgHom.id R S) (x : P), ↑((derivationOfSectionOfKerSqZero f hf' g hg) x) = x - g (f x)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.coe_zero : ∀ {α : Type u_2} [inst : Zero α], ↑0 = 0
-- Mathlib.Algebra.Star.StarRingHom
/-- A *⋆-ring* equivalence is an equivalence preserving addition, multiplication, and the star
operation, which allows for considering both unital and non-unital equivalences with a single
structure.  -/
«term_≃⋆+*_» : Lean.TrailingParserDescr
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.augmentOfIsInitial_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {T : C}
  (hT : CategoryTheory.Limits.IsInitial T), (X.augmentOfIsInitial hT).right = X
-- Lean.Server.CodeActions.Attr
Lean.CodeAction.insertBuiltin : Array Lean.Name → Lean.CodeAction.CommandCodeAction → IO Unit
-- Lean.Parser.Extension
Lean.Parser.instCoeParserParserAliasValue : Coe Lean.Parser.Parser Lean.Parser.ParserAliasValue
-- Mathlib.Topology.AlexandrovDiscrete
isClosed_sUnion : ∀ {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α] {S : Set (Set α)},
  (∀ s ∈ S, IsClosed s) → IsClosed (⋃₀ S)
-- Mathlib.Tactic.SetNotationForOrder
/-- Elaborate a notation like `a ⊆ b` by elaborating `a` and `b`, and then deciding
based on their type whether to return `a ⊆ b` or `a ≤ b`.
Use `a ≤ b` whenever `useSetNotationFor` returns true for the type.
If the type is not known, elaboration of this term is postponed.

We assume that `le` and `sub` are names for declarations of exactly the form
`decl.{u} {α : Type u} [Cls.{u} α] (a b : α) : Prop`, and that likewise `leCls` and `subCls` are
names for declarations of exactly the form  `Cls.{u} (α : Type u) : Type u`.  -/
_private.Mathlib.Tactic.SetNotationForOrder.0.Mathlib.Meta.SetNotationForOrder.elabSubsetLike : Lean.Term → Lean.Term → Lean.Name → Lean.Name → Lean.Name → Lean.Name → Option Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.isLongestMatch_iff : ∀ {c : Char} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatch c pos ↔
    ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ s.startPos.get h = c
-- Mathlib.Analysis.Normed.Group.Basic
NormedGroup.induced.eq_1 : ∀ {𝓕 : Type u_1} (E : Type u_5) (F : Type u_6) [inst : FunLike 𝓕 E F] [inst_1 : Group E] [inst_2 : NormedGroup F]
  [inst_3 : MonoidHomClass 𝓕 E F] (f : 𝓕) (h : Function.Injective ⇑f),
  NormedGroup.induced E F f h =
    { norm := fun a => ‖f a‖, toGroup := inst_1, dist := fun a a_1 => dist (f a) (f a_1), dist_self := ⋯,
      dist_comm := ⋯, dist_triangle := ⋯, edist := fun a a_1 => PseudoMetricSpace.edist (f a) (f a_1), edist_dist := ⋯,
      toUniformSpace :=
        { toTopologicalSpace := TopologicalSpace.induced (⇑f) PseudoMetricSpace.toUniformSpace.toTopologicalSpace,
          uniformity := Filter.comap (fun p => (f p.1, f p.2)) (uniformity F), symm := ⋯, comp := ⋯,
          nhds_eq_comap_uniformity := ⋯ },
      uniformity_dist := ⋯, toBornology := { cobounded := Filter.comap (⇑f) (Bornology.cobounded F), le_cofinite := ⋯ },
      cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
-- Mathlib.Data.Nat.Log
Nat.log_monotone : ∀ {b : ℕ}, Monotone (Nat.log b)
-- Mathlib.Data.Matrix.PEquiv
PEquiv.vecMul_toMatrix_toPEquiv : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : DecidableEq n] [inst_1 : Fintype m] [inst_2 : NonAssocSemiring α]
  (σ : m ≃ n) (a : m → α), Matrix.vecMul a σ.toPEquiv.toMatrix = a ∘ ⇑σ.symm
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonSemanticTokenModifier : Lean.FromJson Lean.Lsp.SemanticTokenModifier
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
IsStrictlyPositive.sqrt : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] (a : A),
  autoParam (IsStrictlyPositive a) IsStrictlyPositive.sqrt._auto_1 → IsStrictlyPositive (CFC.sqrt a)
-- Mathlib.MeasureTheory.Integral.Bochner.Set
/-- For `f : Lp E p μ`, we can define an element of `Lp E p (μ.restrict s)` by
`(Lp.memLp f).restrict s).toLp f`. This map commutes with scalar multiplication.  -/
MeasureTheory.Lp_toLp_restrict_smul : ∀ {X : Type u_1} {F : Type u_4} {mX : MeasurableSpace X} {𝕜 : Type u_5} [inst : NormedRing 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : Module 𝕜 F] [inst_3 : IsBoundedSMul 𝕜 F] {p : ENNReal}
  {μ : MeasureTheory.Measure X} (c : 𝕜) (f : ↥(MeasureTheory.Lp F p μ)) (s : Set X),
  MeasureTheory.MemLp.toLp ↑↑(c • f) ⋯ = c • MeasureTheory.MemLp.toLp ↑↑f ⋯
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.ext_iff : ∀ {A : Type u_2} {B : Type u_3} [inst : Mul A] [inst_1 : Mul B] [inst_2 : Star A] [inst_3 : Star B] {f g : A ≃⋆* B},
  f = g ↔ ∀ (a : A), f a = g a
-- Qq.Typ
/-- `QuotedDefEq lhs rhs` says that the expressions `lhs` and `rhs` are definitionally equal.

You should usually write this using the notation `$lhs =Q $rhs`.
 -/
Qq.QuotedDefEq : {u : Lean.Level} → {α : Q(Sort u)} → Q(«$α») → Q(«$α») → Prop
-- Mathlib.Order.Heyting.Basic
gc_sdiff_sup : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a : α}, GaloisConnection (fun x => x \ a) fun x => a ⊔ x
-- Mathlib.Geometry.Manifold.Submersion
/-- If `f` is a submersion w.r.t. some complement `F`, it is a submersion.

Note that the proof contains a small formalisation-related subtlety: `F` can live in any universe,
while being a submersion requires the existence of a complement in the same universe as
the model normed space of `N`. This is solved by `smallComplement` and `smallEquiv`.
 -/
Manifold.IsSubmersionOfComplement.isSubmersion : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : TopologicalSpace H] [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace H M] [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N},
  Manifold.IsSubmersionOfComplement F I J n f → Manifold.IsSubmersion I J n f
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.norm_integral_min_max : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ}
  (f : ℝ → E), ‖∫ (x : ℝ) in min a b..max a b, f x ∂μ‖ = ‖∫ (x : ℝ) in a..b, f x ∂μ‖
-- Batteries.Data.String.Lemmas
Substring.Raw.ValidFor.of_eq : ∀ {l m r : List Char} (s : Substring.Raw),
  s.str.toList = l ++ m ++ r →
    s.startPos.byteIdx = String.utf8Len l →
      s.stopPos.byteIdx = String.utf8Len l + String.utf8Len m → Substring.Raw.ValidFor l m r s
-- Init.Data.SInt.Basic
instComplementInt16 : Complement Int16
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- A multivariate polynomial `φ` is weighted homogeneous of weighted degree `m` if all monomials
occurring in `φ` have weighted degree `m`.  -/
MvPolynomial.IsWeightedHomogeneous : {R : Type u_1} →
  {M : Type u_2} → [inst : CommSemiring R] → {σ : Type u_3} → [AddCommMonoid M] → (σ → M) → MvPolynomial σ R → M → Prop
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.ceil_lt_mul : ∀ {x : ℝ}, 50 / 19 ≤ x → ↑⌈x⌉₊ < 1.38 * x
-- Mathlib.MeasureTheory.OuterMeasure.Basic
MeasureTheory.measure_union_le : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F}
  (s t : Set α), μ (s ∪ t) ≤ μ s + μ t
-- Mathlib.Algebra.Group.Basic
sub_add_sub_comm : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b c d : α), a - b + (c - d) = a + c - (b + d)
-- Mathlib.RingTheory.PowerSeries.Evaluation
PowerSeries.hasEvalIdeal.eq_1 : ∀ {S : Type u_2} [inst : CommRing S] [inst_1 : TopologicalSpace S] [inst_2 : IsTopologicalRing S]
  [inst_3 : IsLinearTopology S S],
  PowerSeries.hasEvalIdeal = { carrier := {a | PowerSeries.HasEval a}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
CategoryTheory.ObjectProperty.limitsClosure_top : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} (J : α → Type u')
  [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)], ⊤.limitsClosure J = ⊤
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.cylinder.ι₀_desc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F K : HomologicalComplex C c} [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasCylinder]
  (φ₀ φ₁ : K ⟶ F) (h : Homotopy φ₀ φ₁),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.ι₀ K) (HomologicalComplex.cylinder.desc φ₀ φ₁ h) = φ₀
-- Lean.Data.Lsp.TextSync
Lean.Lsp.DidChangeTextDocumentParams.mk : Lean.Lsp.VersionedTextDocumentIdentifier →
  Array Lean.Lsp.TextDocumentContentChangeEvent → Lean.Lsp.DidChangeTextDocumentParams
-- Mathlib.Tactic.Order.ToInt
Mathlib.Tactic.Order.ToInt.toInt_nlt_toInt : ∀ {α : Type u_1} [inst : LinearOrder α] {n : ℕ} (val : Fin n → α) (i j : Fin n),
  ¬Mathlib.Tactic.Order.ToInt.toInt val i < Mathlib.Tactic.Order.ToInt.toInt val j ↔ ¬val i < val j
-- Mathlib.Computability.Primrec.Basic
Primrec.nat_casesOn : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {f : α → ℕ} {g : α → β} {h : α → ℕ → β},
  Primrec f → Primrec g → Primrec₂ h → Primrec fun a => Nat.casesOn (f a) (g a) (h a)
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_reverse : ∀ {w i : ℕ} {x : BitVec w}, x.reverse.getLsbD i = x.getMsbD i
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
IsSymmetricAlgebra.lift_eq : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_3}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] {f : M →ₗ[R] A} (h : IsSymmetricAlgebra f) {A' : Type u_4}
  [inst_5 : CommSemiring A'] [inst_6 : Algebra R A'] (g : M →ₗ[R] A') (a : M), (h.lift g) (f a) = g a
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get?_eq_getElem? : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α}, m.get? a = m[a]?
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instHashableResolvableCompletionItem : Hashable Lean.Lsp.ResolvableCompletionItem
-- Mathlib.RingTheory.HahnSeries.Lex
HahnSeries.instLinearOrderLex : {Γ : Type u_1} →
  {R : Type u_2} → [inst : LinearOrder Γ] → [inst_1 : Zero R] → [LinearOrder R] → LinearOrder (Lex (HahnSeries Γ R))
-- Mathlib.Algebra.Category.ModuleCat.Products
ModuleCat.piIsoPi_hom_ker_subtype : ∀ {R : Type u} [inst : Ring R] {ι : Type v} (Z : ι → ModuleCat R) [inst_1 : CategoryTheory.Limits.HasProduct Z] (i : ι),
  CategoryTheory.CategoryStruct.comp (ModuleCat.piIsoPi Z).hom (ModuleCat.ofHom (LinearMap.proj i)) =
    CategoryTheory.Limits.Pi.π Z i
-- Mathlib.Algebra.Order.Monovary
/-- Two functions monovary iff the rearrangement inequality holds.  -/
monovary_iff_mul_rearrangement : ∀ {ι : Type u_1} {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {f g : ι → α},
  Monovary f g ↔ ∀ (i j : ι), f i * g j + f j * g i ≤ f i * g i + f j * g j
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coeIdeal_inf : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [FaithfulSMul R P] (I J : Ideal R), ↑(I ⊓ J) = ↑I ⊓ ↑J
-- Init.Data.Sum.Lemmas
Sum.Lex.mono : ∀ {α : Type u_1} {r₁ r₂ : α → α → Prop} {β : Type u_2} {s₁ s₂ : β → β → Prop} {x y : α ⊕ β},
  (∀ (a b : α), r₁ a b → r₂ a b) → (∀ (a b : β), s₁ a b → s₂ a b) → Sum.Lex r₁ s₁ x y → Sum.Lex r₂ s₂ x y
-- Mathlib.AlgebraicGeometry.Restrict
/-- The open sets of an open subscheme corresponds to the open sets containing in the subset.  -/
AlgebraicGeometry.opensRestrict : {X : AlgebraicGeometry.Scheme} → (U : X.Opens) → (↑U).Opens ≃ { V // V ≤ U }
-- Lean.Widget.Diff
_private.Lean.Widget.Diff.0.Lean.Widget.instAppendExprDiff : Append Lean.Widget.ExprDiff✝
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.instNorm : {α : Type u_1} →
  {E : Type u_3} → [inst : TopologicalSpace α] → [CompactSpace α] → [inst_2 : SeminormedAddCommGroup E] → Norm C(α, E)
-- Mathlib.Algebra.Group.Basic
neg_sub_neg : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b : α), -a - -b = b - a
-- Mathlib.Analysis.Distribution.DerivNotation
LineDeriv.iteratedLineDerivOp_fin_zero : ∀ {V : Type u_11} {E : Type u_12} [inst : LineDeriv V E E] (m : Fin 0 → V) (f : E),
  LineDeriv.iteratedLineDerivOp m f = f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α}, k ∉ t₁ → (t₁ ∩ t₂).get? k = none
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.Slice.skipSuffix?_string_eq_some_iff' : ∀ {pat : String} {s : String.Slice} {pos : s.Pos}, s.skipSuffix? pat = some pos ↔ ∃ t, pos.Splits t pat
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.Integrable.comp_snd_iff : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  [MeasureTheory.IsFiniteMeasure μ] {f : β → E},
  μ ≠ 0 → (MeasureTheory.Integrable (fun x => f x.2) (μ.prod ν) ↔ MeasureTheory.Integrable f ν)
-- Mathlib.Data.Multiset.Basic
/-- Given a proof `hp` that there exists a unique `a ∈ l` such that `p a`, `chooseX p l hp` returns
that `a` together with proofs of `a ∈ l` and `p a`.  -/
Multiset.chooseX : {α : Type u_1} → (p : α → Prop) → [DecidablePred p] → (l : Multiset α) → (∃! a, a ∈ l ∧ p a) → { a // a ∈ l ∧ p a }
-- Mathlib.Topology.ExtremallyDisconnected
/-- The closure of every open set is open.  -/
ExtremallyDisconnected.open_closure : ∀ {X : Type u} {inst : TopologicalSpace X} [self : ExtremallyDisconnected X] (U : Set X), IsOpen U → IsOpen (closure U)
-- Mathlib.GroupTheory.Commutator.Basic
/-- **The Hall-Witt identity**  -/
addConj_addCommutatorElement_left_addCommutatorElement_add : ∀ {G : Type u_1} [inst : AddGroup G] (a b c : G),
  a + ⁅⁅-a, b⁆, c⁆ + -a + c + ⁅⁅-c, a⁆, b⁆ + -c + b + ⁅⁅-b, c⁆, a⁆ + -b = 0
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.IsWeightedHomogeneous.weightedHomogeneousComponent_ne : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] {w : σ → M} {m : M}
  (n : M) {p : MvPolynomial σ R},
  MvPolynomial.IsWeightedHomogeneous w p m → n ≠ m → (MvPolynomial.weightedHomogeneousComponent w n) p = 0
-- Mathlib.RingTheory.Ideal.Colon
Submodule.annihilator_map_mkQ_eq_colon : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N P : Submodule R M},
  (Submodule.map N.mkQ P).annihilator = N.colon ↑P
-- Lean.Data.Lsp.Workspace
Lean.Lsp.FileEvent : Type
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.empty_mem_measurableCylinders : ∀ {ι : Type u_2} (α : ι → Type u_1) [inst : (i : ι) → MeasurableSpace (α i)], ∅ ∈ MeasureTheory.measurableCylinders α
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.self_le_maxKey!_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {v : β}, (cmp k (t.insertIfNew k v).maxKey!).isLE = true
-- Mathlib.Combinatorics.SimpleGraph.Tutte
/-- Proves the necessity part of Tutte's theorem  -/
SimpleGraph.not_isTutteViolator_of_isPerfectMatching : ∀ {V : Type u_1} {G : SimpleGraph V} [Finite V] {M : G.Subgraph},
  M.IsPerfectMatching → ∀ (u : Set V), ¬G.IsTutteViolator u
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.instLattice.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : SeparatelyContinuousMul G],
  OpenSubgroup.instLattice =
    { toSemilatticeSup := Function.Injective.semilatticeSup OpenSubgroup.toSubgroup ⋯ ⋯ ⋯ ⋯, inf := SemilatticeInf.inf,
      inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.isoBiprodZero_inv : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] (hY : CategoryTheory.Limits.IsZero Y),
  (CategoryTheory.Limits.isoBiprodZero hY).inv = CategoryTheory.Limits.biprod.fst
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.divRight_toEquiv : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricSMul Gᵐᵒᵖ G] (c : G),
  (IsometryEquiv.divRight c).toEquiv = Equiv.divRight c
-- Mathlib.Combinatorics.Matroid.Rank.Finite
/-- A set satisfies `IsRkFinite` iff it has a finite basis'  -/
Matroid.isRkFinite_iff_exists_isBasis' : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, M.IsRkFinite X ↔ ∃ I, M.IsBasis' I X ∧ I.Finite
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.Precylinder.op_p₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.Precylinder A),
  P.op.p₁ = P.i₁.op
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wfImp_insertMany : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {ρ : Type w}
  [inst_4 : ForIn Id ρ ((a : α) × β a)] {m : Std.DHashMap.Internal.Raw₀ α β} {l : ρ},
  Std.DHashMap.Internal.Raw.WFImp ↑m → Std.DHashMap.Internal.Raw.WFImp ↑↑(m.insertMany l)
-- Mathlib.Order.RelIso.Basic
RelHom.id_apply : ∀ {α : Type u_1} (r : α → α → Prop) (x : α), (RelHom.id r) x = x
-- Plausible.Gen
/-- Choose a `Nat` between `0` and `getSize`.
 -/
Plausible.Gen.chooseNat : Plausible.Gen ℕ
-- Lean.Meta.Tactic.Grind.Arith.Linear.PP
Lean.Meta.Grind.Arith.Linear.pp? : Lean.Meta.Grind.Goal → Lean.MetaM (Option Lean.MessageData)
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.IsDiameter.midpoint_eq_center : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
  s.IsDiameter p₁ p₂ → midpoint ℝ p₁ p₂ = s.center
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.Precomp.map.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C}
  (f f_1 : X ⟶ F.left),
  f = f_1 →
    ∀ (i j : Fin (n + 1 + 1)) (x : i ≤ j),
      CategoryTheory.ComposableArrows.Precomp.map F f i j x = CategoryTheory.ComposableArrows.Precomp.map F f_1 i j x
-- Mathlib.Topology.MetricSpace.Dilation
/-- Ratio of the composition `g.comp f` of two dilations is the product of their ratios. We assume
that there exist two points in `α` at extended distance neither `0` nor `∞` because otherwise
`Dilation.ratio (g.comp f) = Dilation.ratio f = 1` while `Dilation.ratio g` can be any number. This
version works for most general spaces, see also `Dilation.ratio_comp` for a version assuming that
`α` is a nontrivial metric space.  -/
Dilation.ratio_comp' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : PseudoEMetricSpace γ] {g : β →ᵈ γ} {f : α →ᵈ β},
  (∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ⊤) → Dilation.ratio (g.comp f) = Dilation.ratio g * Dilation.ratio f
-- Mathlib.SetTheory.Cardinal.NatCount
Nat.count_le_cardinal : ∀ {p : ℕ → Prop} [inst : DecidablePred p] (n : ℕ), ↑(Nat.count p n) ≤ Cardinal.mk ↑{k | p k}
-- ProofWidgets.Data.Html
ProofWidgets.Jsx.delabHtmlOfComponent' : Lean.PrettyPrinter.Delaborator.DelabM (Lean.TSyntax `proofWidgetsJsxElement)
-- Mathlib.GroupTheory.Divisible
Group.rootableByNatOfRootableByInt.eq_1 : ∀ (A : Type u_1) [inst : Group A] [inst_1 : RootableBy A ℤ],
  Group.rootableByNatOfRootableByInt A = { root := fun a n => RootableBy.root a ↑n, root_zero := ⋯, root_cancel := ⋯ }
-- Init.Data.Rat.Lemmas
Rat.zero_add : ∀ (a : ℚ), 0 + a = a
-- Mathlib.Algebra.Order.Field.Basic
uniform_continuous_npow_on_bounded : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (B : α) {ε : α},
  0 < ε → ∀ (n : ℕ), ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_diff_eq_false_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₁.contains k = false → (m₁.diff m₂).contains k = false
-- Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane
EuclideanGeometry.image_inversion_sphere_dist_center : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {c y : P} {R : ℝ},
  R ≠ 0 →
    y ≠ c →
      EuclideanGeometry.inversion c R '' Metric.sphere y (dist y c) =
        insert c ↑(AffineSubspace.perpBisector c (EuclideanGeometry.inversion c R y))
-- Mathlib.Analysis.Convex.Strong
/-- A function `f` from a real normed space is uniformly concave with modulus `φ` if
`t • f x + (1 - t) • f y + t * (1 - t) * φ ‖x - y‖ ≤ f (t • x + (1 - t) • y)` for all `t ∈ [0, 1]`.

`φ` is usually taken to be a monotone function such that `φ r = 0 ↔ r = 0`.  -/
UniformConcaveOn : {E : Type u_1} → [inst : NormedAddCommGroup E] → [NormedSpace ℝ E] → Set E → (ℝ → ℝ) → (E → ℝ) → Prop
-- Std.Do.PostCond
Std.Do.PostShape.pure.sizeOf_spec : sizeOf Std.Do.PostShape.pure = 1
-- Mathlib.CategoryTheory.Sites.Point.Basic
/-- Given `J` a Grothendieck topology on a category `C`, a point of the site `(C, J)`
consists of a functor `fiber : C ⥤ Type w` such that the category `fiber.Elements`
is initially small (which allows defining the fiber functor on presheaves by
taking colimits) and cofiltered (so that the fiber functor on presheaves is exact),
and such that covering sieves induce jointly surjective maps on fibers (which
allows to show that the fibers of a presheaf and its associated sheaf are isomorphic).  -/
CategoryTheory.GrothendieckTopology.Point : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.GrothendieckTopology C → Type (max (max u v) (w + 1))
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.instToJsonInitializeResult : Lean.ToJson Lean.Lsp.InitializeResult
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_ofList_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v fallback : β},
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l → (Std.ExtTreeMap.ofList l cmp).getD k' fallback = v