mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Match.Basic
/-- Pending constraints `lhs ≋ rhs` that need to be solved before the alternative
is considered acceptable. We generate them when processing inaccessible patterns.
Note that `lhs` and `rhs` often have different types.
After we perform additional case analysis, their types become definitionally equal.
 -/
Lean.Meta.Match.Alt.cnstrs : Lean.Meta.Match.Alt → List (Lean.Expr × Lean.Expr)
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestMatch.of_eq : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s t : String.Slice} {pos : s.Pos}
  {pos' : t.Pos},
  String.Slice.Pattern.Model.IsLongestMatch pat pos →
    ∀ (h₁ : s.copy = t.copy), pos.cast h₁ = pos' → String.Slice.Pattern.Model.IsLongestMatch pat pos'
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.mop_hom_rightUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom.mop =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor { unmop := X }).hom
-- Mathlib.RingTheory.LocalProperties.Submodule
Submodule.le_of_isLocalized_span : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set R),
  Ideal.span s = ⊤ →
    ∀ (Mₚ : ↑s → Type u_5) [inst_3 : (r : ↑s) → AddCommMonoid (Mₚ r)] [inst_4 : (r : ↑s) → Module R (Mₚ r)]
      (f : (r : ↑s) → M →ₗ[R] Mₚ r) [inst_5 : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)] {N P : Submodule R M},
      (∀ (r : ↑s),
          Submodule.localized₀ (Submonoid.powers ↑r) (f r) N ≤ Submodule.localized₀ (Submonoid.powers ↑r) (f r) P) →
        N ≤ P
-- Lean.Elab.PreDefinition.Structural.FindRecArg
/-- Collects the `RecArgInfos` for one function, and returns a report for why the others were not
considered.

The `xs` are the fixed parameters, `value` the body with the fixed prefix instantiated.

Takes the optional user annotation into account (`termMeasure?`). If this is given and the measure
is unsuitable, throw an error.
 -/
Lean.Elab.Structural.getRecArgInfos : Lean.Name →
  Lean.Elab.FixedParamPerm →
    Array Lean.Expr →
      Lean.Expr →
        Option Lean.Elab.TerminationMeasure → Lean.MetaM (Array Lean.Elab.Structural.RecArgInfo × Lean.MessageData)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
PresheafOfModules.colimitCocone_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R))
  [inst_2 :
    ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
      CategoryTheory.Limits.PreservesColimit (F.comp (PresheafOfModules.evaluation R Y))
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))]
  [inst_3 : ∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))],
  (PresheafOfModules.colimitCocone F).pt = PresheafOfModules.colimitPresheafOfModules F
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorAdd_zero_add_inv_app : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (a : A) (X : C),
  (CategoryTheory.shiftFunctorAdd C 0 a).inv.app X =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctor C a).map ((CategoryTheory.shiftFunctorZero C A).hom.app X))
      (CategoryTheory.eqToHom ⋯)
-- Mathlib.Topology.Homotopy.TopCat.Path
/-- Given two points `x` and `y` of `X : TopCat`, this is the type
of paths from `x` to `y`, defined using a morphism `I ⟶ X`.
Set `TopCat.pathEquiv` for the relation with `_root_.Path x y`.  -/
TopCat.Path : (X : TopCat) → ↑X → ↑X → Type u
-- Mathlib.Analysis.Calculus.Deriv.Add
hasDerivAtFilter_add_const_iff : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {L : Filter (𝕜 × 𝕜)} (c : F),
  HasDerivAtFilter (fun x => f x + c) f' L ↔ HasDerivAtFilter f f' L
-- Mathlib.FieldTheory.IntermediateField.Basic
AlgHom.mem_fieldRange : ∀ {K : Type u_1} {L : Type u_2} {L' : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Field L']
  [inst_3 : Algebra K L] [inst_4 : Algebra K L'] {f : L →ₐ[K] L'} {y : L'}, y ∈ f.fieldRange ↔ ∃ x, f x = y
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- `G.IsBipartite` if and only if `G.IsBipartiteWith s t`.  -/
SimpleGraph.isBipartite_iff_exists_isBipartiteWith : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsBipartite ↔ ∃ s t, G.IsBipartiteWith s t
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
CategoryTheory.Limits.Types.pushoutCocone_inr_injective_of_isColimit : ∀ {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} {c : CategoryTheory.Limits.PushoutCocone f g}
  (hc : CategoryTheory.Limits.IsColimit c),
  Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f) →
    Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom c.inr)
-- Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
Algebra.Generators.cotangentCompLocalizationAwayEquiv.eq_1 : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (g : S) [inst_7 : IsLocalization.Away g T] (P : Algebra.Generators R S ι)
  {x : ((Algebra.Generators.localizationAway T g).comp P).toExtension.Cotangent}
  (hx :
    (Algebra.Extension.Cotangent.map ((Algebra.Generators.localizationAway T g).ofComp P).toExtensionHom) x =
      Algebra.Generators.cMulXSubOneCotangent T g),
  Algebra.Generators.cotangentCompLocalizationAwayEquiv g P hx =
    ↑((⋯.splitSurjectiveEquiv ⋯) ⟨Algebra.Generators.cotangentCompAwaySec g P x, ⋯⟩)
-- Mathlib.Logic.Basic
/-- **Alias** of `by_contradiction`. -/
by_contra : ∀ {p : Prop}, (¬p → False) → p
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
sineTerm_ne_zero : ∀ {x : ℂ}, x ∈ Complex.integerComplement → ∀ (n : ℕ), 1 + sineTerm x n ≠ 0
-- Mathlib.Data.Int.Fib.Basic
Int.fib_neg_natCast : ∀ (n : ℕ), Int.fib (-↑n) = (-1) ^ (n + 1) * ↑(Nat.fib n)
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.D₁.ιRight.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {Z : C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] {X Y : C} (f f_1 : X ⟶ Y)
  (e_f : f = f_1) (hf : W f) (g g_1 : X ⟶ Z),
  g = g_1 →
    CategoryTheory.OrthogonalReflection.D₁.ιRight f hf g = CategoryTheory.OrthogonalReflection.D₁.ιRight f_1 ⋯ g_1
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min?_eq_some_min! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α],
  t ≠ ∅ → t.min? = some t.min!
-- Mathlib.Order.Filter.Extr
IsMinFilter.congr : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f g : α → β} {a : α} {l : Filter α},
  IsMinFilter f l a → f =ᶠ[l] g → f a = g a → IsMinFilter g l a
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_union_of_contains_eq_false_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF →
    (↑m₂).WF →
      ∀ {k : α},
        m₁.contains k = false →
          Std.DHashMap.Internal.Raw₀.Const.get? (m₁.union m₂) k = Std.DHashMap.Internal.Raw₀.Const.get? m₂ k
-- Init.Data.SInt.Basic
/-- Negates 64-bit signed integers. Usually accessed via the `-` prefix operator.

This function is overridden at runtime with an efficient implementation.
 -/
Int64.neg : Int64 → Int64
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
ProbabilityTheory.Kernel.partialTraj_succ_eq_comp : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} {a b : ℕ}
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))},
  a ≤ b →
    ProbabilityTheory.Kernel.partialTraj κ a (b + 1) =
      (ProbabilityTheory.Kernel.partialTraj κ b (b + 1)).comp (ProbabilityTheory.Kernel.partialTraj κ a b)
-- Init.Data.Int.DivMod.Lemmas
Int.bmod_neg_iff : ∀ {m : ℕ} {x : ℤ}, -↑m ≤ x → x < ↑m → (x.bmod m < 0 ↔ -(↑m / 2) ≤ x ∧ x < 0 ∨ (↑m + 1) / 2 ≤ x)
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.map_injective : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} {B : Type u_6} {f : A → B},
  Function.Injective f → Function.Injective fun M => M.map f
-- Mathlib.Tactic.Linter.DeprecatedSyntaxLinter
/-- The deprecated syntax linter flags usages of deprecated syntax and suggests
replacement syntax. For each individual case, linting can be turned on or off separately.

* `refine'`, superseded by `refine` and `apply` (controlled by `linter.style.refine`)
* `cases'`, superseded by `obtain`, `rcases` and `cases` (controlled by `linter.style.cases`)
* `induction'`, superseded by `induction` (controlled by `linter.style.induction`)
* `admit`, superseded by `sorry` (controlled by `linter.style.admit`)
* `set_option maxHeartbeats`, should contain an explanatory comment
  (controlled by `linter.style.maxHeartbeats`)
 -/
_private.Mathlib.Tactic.Linter.DeprecatedSyntaxLinter.0.Mathlib.Linter.Style.deprecatedSyntaxLinter : Lean.Linter
-- Mathlib.Order.Defs.Unbundled
IsLowerSet.eq_1 : ∀ {α : Type u_1} [inst : LE α] (s : Set α), IsLowerSet s = ∀ ⦃a b : α⦄, b ≤ a → a ∈ s → b ∈ s
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.applyAsHom_comm_apply : ∀ {k : Type u} [inst : Semiring k] {G : Type v} [inst_1 : CommMonoid G] {A B : Rep.{u_1, u, v} k G} (f : A ⟶ B) (g : G)
  (x : ↑A), (CategoryTheory.ConcreteCategory.hom f) ((A.ρ g) x) = (B.ρ g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Mathlib.Data.Nat.Factorial.BigOperators
_private.Mathlib.Data.Nat.Factorial.BigOperators.0.Nat.factorial.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.RingTheory.Bialgebra.Basic
/-- The comultiplication on a bialgebra preserves `1`.  -/
Bialgebra.comul_one : ∀ {R : Type u} {A : Type v} {inst : CommSemiring R} {inst_1 : Semiring A} [self : Bialgebra R A],
  CoalgebraStruct.comul 1 = 1
-- Init.Data.Nat.Basic
Nat.instNeZeroHPowOfNat : ∀ {n : ℕ}, NeZero (n ^ 0)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.instDecidableEqWalkingParallelPairHom.decEq : {a a_1 : CategoryTheory.Limits.WalkingParallelPair} →
  (x x_1 : CategoryTheory.Limits.WalkingParallelPairHom a a_1) → Decidable (x = x_1)
-- Mathlib.Analysis.Normed.Ring.Basic
one_le_nnnorm_one : ∀ (β : Type u_5) [inst : NormedRing β] [Nontrivial β], 1 ≤ ‖1‖₊
-- Mathlib.Geometry.Manifold.Bordism
SingularManifold.instIsManifoldRealM : ∀ {X : Type u_1} [inst : TopologicalSpace X] {k : WithTop ℕ∞} {E : Type u_4} {H : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : FiniteDimensional ℝ E]
  [inst_4 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {s : SingularManifold X k I}, IsManifold I k s.M
-- Mathlib.Topology.Order.AtTopBotIxx
comap_coe_nhdsLT_of_Ioo_subset : ∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] {s : Set X} {b : X},
  s ⊆ Set.Iio b →
    (s.Nonempty → ∃ a < b, Set.Ioo a b ⊆ s) →
      autoParam (Order.IsSuccPrelimit b) comap_coe_nhdsLT_of_Ioo_subset._auto_1 →
        Filter.comap Subtype.val (nhdsWithin b (Set.Iio b)) = Filter.atTop
-- Mathlib.Analysis.Convex.Basic
convex_iff_ordConnected : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜},
  Convex 𝕜 s ↔ s.OrdConnected
-- Lean.Data.NameMap.Basic
Lean.NameSSet.empty : Lean.NameSSet
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.swap_toFun : ∀ (A : Type u_2) (B : Type u_3) [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] (i : A × B), (ContinuousMonoidHom.swap A B) i = (i.2, i.1)
-- Mathlib.Algebra.Regular.ULift
ULift.isLeftRegular_down : ∀ {R : Type v} [inst : Mul R] {a : ULift.{u, v} R}, IsLeftRegular a.down ↔ IsLeftRegular a
-- Mathlib.Algebra.Polynomial.BigOperators
/-- The degree of a product of polynomials is equal to
the sum of the degrees, provided that the product of leading coefficients is nonzero.

See `Polynomial.natDegree_prod` (without the `'`) for a version for integral domains,
where this condition is automatically satisfied.
 -/
Polynomial.natDegree_prod' : ∀ {R : Type u} {ι : Type w} (s : Finset ι) [inst : CommSemiring R] (f : ι → Polynomial R),
  ∏ i ∈ s, (f i).leadingCoeff ≠ 0 → (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.below.whiskerRight : ∀ {C : Type u}
  {motive :
    {X Y : CategoryTheory.FreeMonoidalCategory C} →
      (a a_1 : X.Hom Y) → CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1 → Prop}
  {Y Z : CategoryTheory.FreeMonoidalCategory C} (f f' : Y.Hom Z) (X : CategoryTheory.FreeMonoidalCategory C)
  (a : CategoryTheory.FreeMonoidalCategory.HomEquiv f f'),
  CategoryTheory.FreeMonoidalCategory.HomEquiv.below a →
    motive f f' a → CategoryTheory.FreeMonoidalCategory.HomEquiv.below ⋯
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.colimitHomIsoLimitYoneda_hom_comp_π_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (F : CategoryTheory.Functor I C) [inst_2 : CategoryTheory.Limits.HasColimit F]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type u₂)] (A : C) (i : I) {Z : Type u₂}
  (h : (CategoryTheory.yoneda.obj A).obj (F.op.obj (Opposite.op i)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitHomIsoLimitYoneda F A).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.limit.π (F.op.comp (CategoryTheory.yoneda.obj A)) (Opposite.op i)) h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.yoneda.obj A).map (CategoryTheory.Limits.colimit.ι F i).op) h
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.up_length_toListRev_eq_length : ∀ {m : Type w → Type u_1} {α β : Type w} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β},
  (fun x => { down := x.length }) <$> it.toListRev = it.length
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.nnnorm_ofSubsingleton : ∀ {𝕜 : Type u} {ι : Type v} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G] [inst_3 : SeminormedAddCommGroup G']
  [inst_4 : NormedSpace 𝕜 G'] [inst_5 : Fintype ι] [inst_6 : Subsingleton ι] (i : ι) (f : G →L[𝕜] G'),
  ‖(ContinuousMultilinearMap.ofSubsingleton 𝕜 G G' i) f‖₊ = ‖f‖₊
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected
/-- Detecting vanishing of a morphism factoring through a connected colimit by pulling back along
the inclusions of the colimit.  -/
CategoryTheory.Limits.IsColimit.pullback_zero_ext : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] [CategoryTheory.IsConnected J] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_4 : CategoryTheory.Limits.HasPullbacks C] [inst_5 : CategoryTheory.Limits.HasColimitsOfShape J C]
  [CategoryTheory.HasExactColimitsOfShape J C] {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F}
  (hc : CategoryTheory.Limits.IsColimit c) {X Y : C} {f : X ⟶ c.pt} {g : c.pt ⟶ Y},
  (∀ (j : J),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (c.ι.app j) f)
          (CategoryTheory.CategoryStruct.comp f g) =
        0) →
    CategoryTheory.CategoryStruct.comp f g = 0
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
LineDifferentiableAt.eq_1 : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] (f : E → F) (x v : E),
  LineDifferentiableAt 𝕜 f x v = DifferentiableAt 𝕜 (fun t => f (x + t • v)) 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
/-- The cosine of `π / 5` is `(1 + √5) / 4`.  -/
Real.cos_pi_div_five : Real.cos (Real.pi / 5) = (1 + √5) / 4
-- Mathlib.LinearAlgebra.AnnihilatingPolynomial
/-- It is useful to refer to ideal membership sometimes
and the annihilation condition other times.  -/
Polynomial.mem_annIdeal_iff_aeval_eq_zero : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {a : A}
  {p : Polynomial R}, p ∈ Polynomial.annIdeal R a ↔ (Polynomial.aeval a) p = 0
-- Mathlib.Algebra.Lie.Prod
LieHom.fst_comp_inr : ∀ (R : Type u_1) (L₁ : Type u_2) (L₂ : Type u_3) [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂], (LieHom.fst R L₁ L₂).comp (LieHom.inr R L₁ L₂) = 0
-- Batteries.Data.List.Lemmas
List.mem_idxsOf_iff_getElem_pos : ∀ {α : Type u_1} {i : ℕ} {xs : List α} {x : α} [inst : BEq α] (hi : i < xs.length),
  i ∈ List.idxsOf x xs ↔ (xs[i] == x) = true
-- Init.Data.UInt.Bitwise
UInt16.toUInt32_xor : ∀ (a b : UInt16), (a ^^^ b).toUInt32 = a.toUInt32 ^^^ b.toUInt32
-- Aesop.Stats.Basic
Aesop.instToJsonRuleStats : Lean.ToJson Aesop.RuleStats
-- Mathlib.RingTheory.SimpleModule.Basic
LinearMap.isSimpleModule_iff_of_bijective : ∀ {R : Type u_2} {S : Type u_3} [inst : Ring R] [inst_1 : Ring S] {M : Type u_4} [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {N : Type u_5} [inst_4 : AddCommGroup N] [inst_5 : Module S N] {σ : R →+* S}
  [RingHomSurjective σ] (l : M →ₛₗ[σ] N), Function.Bijective ⇑l → (IsSimpleModule R M ↔ IsSimpleModule S N)
-- Mathlib.Algebra.GradedMonoid
SetLike.one_mem_graded : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst_1 : One R] [inst_2 : Zero ι] (A : ι → S)
  [SetLike.GradedOne A], 1 ∈ A 0
-- Lean.Expr
_private.Lean.Expr.0.Lean.intLTPred : Lean.Expr
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.neighborSet_eq_empty : ∀ {V : Type u} (G : SimpleGraph V) {v : V}, G.neighborSet v = ∅ ↔ G.IsIsolated v
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.builder_nameDestruct : Lean.ParserDescr
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.isEmpty_eq : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  m₁.Equiv m₂ → m₁.isEmpty = m₂.isEmpty
-- Std.Data.HashMap.Raw
/-- Checks whether a key is present in a map and inserts a value for the key if it was not found.

If the returned `Bool` is `true`, then the returned map is unaltered. If the `Bool` is `false`, then
the returned map has a new value inserted.

Equivalent to (but potentially faster than) calling `contains` followed by `insertIfNew`.
 -/
Std.HashMap.Raw.containsThenInsertIfNew : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → Std.HashMap.Raw α β → α → β → Bool × Std.HashMap.Raw α β
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.single_injective : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] {i : ι},
  Function.Injective (DFinsupp.single i)
-- Init.Data.Float.Model.Format.Basic
Float.Model.Format.mk.injEq : ∀ (mantissaBitsWithoutImplicit : ℕ) (hm : autoParam (0 < mantissaBitsWithoutImplicit) Float.Model.Format.hm._autoParam)
  (exponentBits : ℕ) (he : autoParam (0 < exponentBits) Float.Model.Format.he._autoParam)
  (mantissaBitsWithoutImplicit_1 : ℕ)
  (hm_1 : autoParam (0 < mantissaBitsWithoutImplicit_1) Float.Model.Format.hm._autoParam) (exponentBits_1 : ℕ)
  (he_1 : autoParam (0 < exponentBits_1) Float.Model.Format.he._autoParam),
  ({ mantissaBitsWithoutImplicit := mantissaBitsWithoutImplicit, hm := hm, exponentBits := exponentBits, he := he } =
      { mantissaBitsWithoutImplicit := mantissaBitsWithoutImplicit_1, hm := hm_1, exponentBits := exponentBits_1,
        he := he_1 }) =
    (mantissaBitsWithoutImplicit = mantissaBitsWithoutImplicit_1 ∧ exponentBits = exponentBits_1)
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.floor_sub_le_translationNumber : ∀ (f : CircleDeg1Lift) (x : ℝ), ↑⌊f x - x⌋ ≤ f.translationNumber
-- Mathlib.LinearAlgebra.Matrix.Reindex
Matrix.toLinearEquiv_reindexAlgEquiv : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_11) (A : Type u_12) [inst : CommSemiring R] [inst_1 : Fintype n]
  [inst_2 : Fintype m] [inst_3 : DecidableEq m] [inst_4 : DecidableEq n] [inst_5 : Semiring A] [inst_6 : Algebra R A]
  (e : m ≃ n), ↑(Matrix.reindexAlgEquiv R A e) = Matrix.reindexLinearEquiv R A e e
-- Mathlib.Topology.EMetricSpace.Defs
edist_le_zero : ∀ {γ : Type w} [inst : EMetricSpace γ] {x y : γ}, edist x y ≤ 0 ↔ x = y
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.ofCLM.injEq : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : Semiring 𝕜₁] [inst_1 : Semiring 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] (toCLM toCLM_1 : E →SL[σ] F),
  (ContinuousLinearMapWOT.ofCLM toCLM = ContinuousLinearMapWOT.ofCLM toCLM_1) = (toCLM = toCLM_1)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCastD_nil : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {a : α} {fallback : β a},
  Std.Internal.List.getValueCastD a [] fallback = fallback
-- Mathlib.Algebra.Lie.Killing
LieAlgebra.IsKilling.ideal_eq_bot_of_isLieAbelian : ∀ {R : Type u_1} {L : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [LieAlgebra.IsKilling R L] [Module.Free R L] [Module.Finite R L] [IsDomain R] [IsPrincipalIdealRing R]
  (I : LieIdeal R L) [IsLieAbelian ↥I], I = ⊥
-- Mathlib.Data.ENNReal.Operations
ENNReal.sub_sub_cancel : ∀ {a b : ENNReal}, a ≠ ⊤ → b ≤ a → a - (a - b) = b
-- Mathlib.Algebra.Pointwise.Stabilizer
MulAction.stabilizer_subgroup : ∀ {G : Type u_1} [inst : Group G] (s : Subgroup G), MulAction.stabilizer G ↑s = s
-- Lean.Elab.Do.Legacy
/-- Generate `CodeBlock` for `doMatchExpr; doElems`  -/
Lean.Elab.Term.Do.ToCodeBlock.doMatchExprToCode : Lean.Syntax → List Lean.Syntax → Lean.Elab.Term.Do.ToCodeBlock.M Lean.Elab.Term.Do.CodeBlock
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- The symbol `J(a | b)` depends only on `a` mod `b`.  -/
jacobiSym.mod_left : ∀ (a : ℤ) (b : ℕ), jacobiSym a b = jacobiSym (a % ↑b) b
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.whiskerLeft_comp_bimod : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C]
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [inst_4 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  {X Y Z : CategoryTheory.Mon C} (M : Bimod X Y) {N P Q : Bimod Y Z} (f : N ⟶ P) (g : P ⟶ Q),
  M.whiskerLeft (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (M.whiskerLeft f) (M.whiskerLeft g)
-- Init.Data.SInt.Lemmas
Int32.neg_inj : ∀ {a b : Int32}, -a = -b ↔ a = b
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MCasesPat.brecOn_1.go : {motive_1 : Lean.Parser.Tactic.MCasesPat → Sort u} →
  {motive_2 : List Lean.Parser.Tactic.MCasesPat → Sort u} →
    (t : List Lean.Parser.Tactic.MCasesPat) →
      ((t : Lean.Parser.Tactic.MCasesPat) → t.below → motive_1 t) →
        ((t : List Lean.Parser.Tactic.MCasesPat) → Lean.Parser.Tactic.MCasesPat.below_1 t → motive_2 t) →
          motive_2 t ×' Lean.Parser.Tactic.MCasesPat.below_1 t
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.boundary_last : ∀ {n : ℕ} (c : Composition n), c.boundary (Fin.last c.length) = Fin.last n
-- Mathlib.Algebra.Group.Units.Equiv
/-- Extra simp lemma that `dsimp` can use. `simp` will never use this.  -/
Equiv.addRight_symm_apply : ∀ {G : Type u_5} [inst : AddGroup G] (a : G), ⇑(Equiv.symm (Equiv.addRight a)) = fun x => x + -a