mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.toAddMonoidHom_injective : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β], Function.Injective OrderAddMonoidHom.toAddMonoidHom
-- Lean.Widget.UserWidget
Lean.Widget.instInhabitedWidgetSource.default : Lean.Widget.WidgetSource
-- Mathlib.Algebra.Lie.TraceForm
LieModule.traceForm_baseChange : ∀ (R : Type u_1) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [Module.Free R M] [Module.Finite R M] (A : Type u_5) [inst_9 : CommRing A] [inst_10 : Algebra R A],
  LieModule.traceForm A (TensorProduct R A L) (TensorProduct R A M) =
    LinearMap.BilinForm.baseChange A (LieModule.traceForm R L M)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `TendstoUniformlyOn.sub` -/
TendstoUniformlyOn.fun_sub : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3}
  {l : Filter ι} {f f' : ι → β → α} {g g' : β → α} {s : Set β},
  TendstoUniformlyOn f g l s →
    TendstoUniformlyOn f' g' l s → TendstoUniformlyOn (fun i i_1 => f i i_1 - f' i i_1) (fun i => g i - g' i) l s
-- Mathlib.Logic.Equiv.Option
Equiv.removeNone_some : ∀ {α : Type u_1} {β : Type u_2} (e : Option α ≃ Option β) {x : α},
  (∃ x', e (some x) = some x') → some (e.removeNone x) = e (some x)
-- Mathlib.Topology.Order.AtTopBotIxx
tendsto_comp_coe_Ioo_atBot : ∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] {a b : X} {α : Type u_2}
  {l : Filter α} {f : X → α},
  a < b →
    autoParam (Order.IsPredPrelimit a) tendsto_comp_coe_Ioo_atBot._auto_1 →
      (Filter.Tendsto (fun x => f ↑x) Filter.atBot l ↔ Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) l)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.toOplax_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.Oplax.StrongTrans F G) {a b : B} (f : a ⟶ b),
  η.toOplax.naturality f = (η.naturality f).hom
-- Mathlib.Data.Set.Subsingleton
Set.nontrivial_mono : ∀ {α : Type u_1} {s t : Set α}, s ⊆ t → Nontrivial ↑s → Nontrivial ↑t
-- Init.Data.Int.DivMod.Lemmas
Int.mul_add_ediv_left : ∀ (b : ℤ) {a : ℤ} (c : ℤ), a ≠ 0 → (a * b + c) / a = b + c / a
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.pp.analyze.explicitHoles : Lean.Option Bool
-- Init.Data.Int.Gcd
Int.gcd_eq_one_iff : ∀ {m n : ℤ}, m.gcd n = 1 ↔ ∀ (c : ℤ), c ∣ m → c ∣ n → c ∣ 1
-- Init.Data.List.Basic
/-- Returns the last element of a non-empty list.

Examples:
* `["circle", "rectangle"].getLast (by decide) = "rectangle"`
* `["circle"].getLast (by decide) = "circle"`
 -/
List.getLast : {α : Type u} → (as : List α) → as ≠ [] → α
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
NonUnitalStarSubalgebra.unitization_apply : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] [inst_6 : SetLike S A]
  [hSA : NonUnitalSubsemiringClass S A] [hSRA : SMulMemClass S R A] [inst_7 : StarMemClass S A] (s : S)
  (x : Unitization R ↥s), (NonUnitalStarSubalgebra.unitization s) x = (algebraMap R A) x.toProd.1 + ↑x.toProd.2
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_sub_const_Icc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b c : α),
  (fun x => x - a) ⁻¹' Set.Icc b c = Set.Icc (b + a) (c + a)
-- Mathlib.SetTheory.Lists
Lists'.atom.inj : ∀ {α : Type u} {a a_1 : α}, Lists'.atom a = Lists'.atom a_1 → a = a_1
-- Lean.Compiler.LCNF.Types
_private.Lean.Compiler.LCNF.Types.0.Lean.Compiler.LCNF.instantiateForall.go : Array Lean.Expr → ℕ → Lean.Expr → Lean.CoreM Lean.Expr
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.ofMatrix_eq_ofMatrixStarAlgEquiv : ∀ {n : Type u_2} {A : Type u_5} [inst : Fintype n] [inst_1 : SMul ℂ A] [inst_2 : Semiring A] [inst_3 : StarRing A],
  ⇑CStarMatrix.ofMatrix = ⇑CStarMatrix.ofMatrixStarAlgEquiv
-- Lean.Meta.Tactic.SplitIf
Lean.Meta.SplitKind.considerIte : Lean.Meta.SplitKind → Bool
-- Init.Data.Int.Linear
Int.Internal.Linear.dvd_le_tight_cert.eq_1 : ∀ (d : ℤ) (p₁ p₂ p₃ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.dvd_le_tight_cert d p₁ p₂ p₃ =
    (Int.blt' 0 d).and'
      ((p₂.beq' ((p₁.addConst_k (-p₁.getConst)).addConst_k p₂.getConst)).and'
        (p₃.beq' ((p₁.addConst_k (-p₁.getConst)).addConst_k (p₁.getConst - d * ((p₁.getConst - p₂.getConst) / d)))))
-- Mathlib.GroupTheory.Perm.Option
map_equiv_removeNone : ∀ {α : Type u_1} [inst : DecidableEq α] (σ : Equiv.Perm (Option α)),
  (Equiv.removeNone σ).optionCongr = Equiv.swap none (σ none) * σ
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.beq' : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Bool
-- Mathlib.Order.Defs.Unbundled
/-- Equality is an equivalence relation.  -/
eq_isEquiv : ∀ (α : Sort u_1), IsEquiv α fun x1 x2 => x1 = x2
-- Mathlib.Topology.Compactness.SigmaCompact
instSigmaCompactSpaceProd : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [SigmaCompactSpace X]
  [SigmaCompactSpace Y], SigmaCompactSpace (X × Y)
-- Lean.Meta.Instances
Lean.Meta.Instances.erase : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → Lean.Meta.Instances → Lean.Name → m Lean.Meta.Instances
-- Mathlib.Data.Stream.Defs
/-- Iterates of a function as a stream.  -/
Stream'.iterate : {α : Type u} → (α → α) → α → Stream' α
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.generateFrom_iUnion : ∀ {X : Type u_1} {ι : Type u_2} {g : ι → Set ((n : ℕ) × (EuclideanSpace ℝ (Fin n) → X))},
  DiffeologicalSpace.generateFrom (⋃ i, g i) = ⨆ i, DiffeologicalSpace.generateFrom (g i)
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.smul_set_compl : ∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] {s : Set β} {a : α}, a • sᶜ = (a • s)ᶜ
-- Init.Meta.Defs
Lean.Syntax.setTailInfoAux : Lean.SourceInfo → Lean.Syntax → Option Lean.Syntax
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegral_fun_smul : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F}
  {γ : Path a b} {𝕝 : Type u_4} [inst_5 : RCLike 𝕝] [inst_6 : NormedSpace 𝕝 F] [inst_7 : SMulCommClass 𝕜 𝕝 F] {c : 𝕝},
  ∫ᶜ (x : E) in γ, c • ω x = c • ∫ᶜ (x : E) in γ, ω x
-- Mathlib.Order.Defs.Unbundled
symm_of : ∀ {α : Sort u_1} (r : α → α → Prop) {a b : α} [Std.Symm r], r a b → r b a
-- Mathlib.Analysis.Convex.Between
/-- **Alias** of the reverse direction of `wbtw_vsub_const_iff`. -/
Wbtw.vsub_const : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y z : P} (p : P), Wbtw R x y z → Wbtw R (x -ᵥ p) (y -ᵥ p) (z -ᵥ p)
-- Mathlib.Algebra.Module.Submodule.IterateMapComap
/-- The `LinearMap.iterateMapComap f i n K : Submodule R N` is
`f⁻¹(i(⋯(f⁻¹(i(K)))))` (`n` times).  -/
LinearMap.iterateMapComap : {R : Type u_1} →
  {N : Type u_2} →
    {M : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid N] →
          [inst_2 : Module R N] →
            [inst_3 : AddCommMonoid M] →
              [inst_4 : Module R M] → (N →ₗ[R] M) → (N →ₗ[R] M) → ℕ → Submodule R N → Submodule R N
-- Mathlib.FieldTheory.Galois.Profinite
InfiniteGalois.proj_adjoin_singleton_val : ∀ {k : Type u_3} {K : Type u_4} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] [inst_3 : IsGalois k K]
  (g : ↑(ProfiniteGrp.limit (InfiniteGalois.asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop) (x : K)
  (y : ↥(FiniteGaloisIntermediateField.adjoin k {x}).toIntermediateField) (L : FiniteGaloisIntermediateField k K)
  (h : x ∈ L.toIntermediateField),
  ↑(((InfiniteGalois.proj (FiniteGaloisIntermediateField.adjoin k {x})) g) y) = ↑(((InfiniteGalois.proj L) g) ⟨↑y, ⋯⟩)
-- Lean.Elab.DefView
/-- The docstring, if present.  -/
Lean.Elab.DefView.docString? : Lean.Elab.DefView → Option (Lean.TSyntax `Lean.Parser.Command.docComment)
-- Init.Data.String.Basic
String.Pos.next_ne_startPos : ∀ {s : String} {p : s.Pos} {h : p ≠ s.endPos}, p.next h ≠ s.startPos
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.mem_sl2SubalgebraOfRoot_iff : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra]
  [inst_5 : LieAlgebra.IsKilling K L] [inst_6 : LieModule.IsTriangularizable K (↥H) L] [inst_7 : CharZero K]
  {α : LieModule.Weight K (↥H) L} (hα : α.IsNonZero) {h e f : L},
  IsSl2Triple h e f →
    e ∈ LieAlgebra.rootSpace H ⇑α →
      f ∈ LieAlgebra.rootSpace H (-⇑α) →
        ∀ {x : L}, x ∈ LieAlgebra.IsKilling.sl2SubalgebraOfRoot hα ↔ ∃ c₁ c₂ c₃, x = c₁ • e + c₂ • f + c₃ • ⁅e, f⁆
-- Init.Sym.Lemmas
Lean.Sym.Fin.eq_eq_false : ∀ {n : ℕ} (a b : Fin n), decide (a = b) = false → (a = b) = False
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.injective_type₂ : ∀ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore), Function.Injective h.type₂
-- Init.MetaTypes
Lean.Meta.Simp.Config.mk : ℕ →
  ℕ →
    Bool →
      Bool →
        Bool →
          Bool →
            Bool →
              Bool →
                Lean.Meta.EtaStructMode →
                  Bool →
                    Bool →
                      Bool →
                        Bool →
                          Bool →
                            Bool →
                              Bool →
                                Bool →
                                  Bool →
                                    Bool →
                                      Bool →
                                        Bool →
                                          Bool →
                                            Bool →
                                              Bool →
                                                Bool →
                                                  Bool →
                                                    Bool → Bool → Bool → Option ℕ → Bool → Bool → Lean.Meta.Simp.Config
-- Mathlib.Algebra.Group.Torsion
Subsingleton.to_isAddTorsionFree : ∀ {M : Type u_1} [inst : AddMonoid M] [Subsingleton M], IsAddTorsionFree M
-- Init.Data.BitVec.Bootstrap
BitVec.toNat_neg : ∀ {n : ℕ} (x : BitVec n), (-x).toNat = (2 ^ n - x.toNat) % 2 ^ n
-- Mathlib.CategoryTheory.Preadditive.Projective.Preserves
CategoryTheory.Functor.preservesProjectiveObjects_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [F.PreservesProjectiveObjects] [G.PreservesProjectiveObjects],
  (F.comp G).PreservesProjectiveObjects
-- Lean.Parser.Term
Lean.Parser.Term.inferInstanceAs.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.MeasureTheory.Measure.SeparableMeasure
MeasureTheory.Measure.MeasureDense.mk : ∀ {X : Type u_1} [m : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝒜 : Set (Set X)},
  (∀ s ∈ 𝒜, MeasurableSet s) →
    (∀ (s : Set X), MeasurableSet s → μ s ≠ ⊤ → ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ (symmDiff s t) < ENNReal.ofReal ε) →
      μ.MeasureDense 𝒜
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.sumInvPow_zero : ∀ (L : PeriodPair), L.sumInvPow 0 = L.G
-- Mathlib.Analysis.Complex.Periodic
Function.Periodic.cuspFunction.eq_1 : ∀ (h : ℝ) (f : ℂ → ℂ),
  Function.Periodic.cuspFunction h f =
    Function.update (f ∘ Function.Periodic.invQParam h) 0
      ((nhdsWithin 0 {0}ᶜ).limUnder (f ∘ Function.Periodic.invQParam h))
-- Mathlib.Topology.UniformSpace.Basic
Uniform.tendsto_congr : ∀ {α : Type u_2} {β : Type u_3} [inst : UniformSpace β] {f g : α → β} {l : Filter α} {b : β},
  Filter.Tendsto (fun x => (f x, g x)) l (uniformity β) → (Filter.Tendsto f l (nhds b) ↔ Filter.Tendsto g l (nhds b))
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.Presieve.overEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (Y : CategoryTheory.Over X)
  (S : CategoryTheory.Presieve Y),
  (CategoryTheory.Presieve.overEquiv Y) S = CategoryTheory.Presieve.map (CategoryTheory.Over.forget X) S
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.inv_mk : ∀ {α : Type u} {L : List (α × Bool)}, (FreeGroup.mk L)⁻¹ = FreeGroup.mk (FreeGroup.invRev L)
-- Mathlib.Logic.Basic
not_imp_comm : ∀ {a b : Prop}, ¬a → b ↔ ¬b → a
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Matrix.GeneralLinearGroup.fixpointPolynomial.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (g : GL (Fin 2) R),
  g.fixpointPolynomial =
    Polynomial.C (↑g 1 0) * Polynomial.X ^ 2 + Polynomial.C (↑g 1 1 - ↑g 0 0) * Polynomial.X - Polynomial.C (↑g 0 1)
-- Mathlib.Analysis.MeanInequalitiesPow
ENNReal.LpAddConst_of_one_le : ∀ {p : ENNReal}, 1 ≤ p → p.LpAddConst = 1
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.coe_inl : ∀ {R : Type u_1} [inst : Semiring R] {M₁ : Type u_2} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R M₁] {M₂ : Type u_3} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂], ↑(ContinuousLinearMap.inl R M₁ M₂) = LinearMap.inl R M₁ M₂
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
/-- Given a `PushoutObjObj` of `f₁ : Arrow C₁` and `f₂ : Arrow C₂`, a `PushoutObjObj` of `f₁'` and
`f₂ : Arrow C₂`, and a morphism `f₁ ⟶ f₁'`, this defines a morphism between the induced
pushout maps.  -/
CategoryTheory.Functor.PushoutObjObj.mapArrowLeft : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} →
              {f₁ f₁' : CategoryTheory.Arrow C₁} →
                {f₂ : CategoryTheory.Arrow C₂} →
                  (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) →
                    (sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom) →
                      (f₁ ⟶ f₁') → (CategoryTheory.Arrow.mk sq₁₂.ι ⟶ CategoryTheory.Arrow.mk sq₁₂'.ι)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.foldlM_eq_foldlM_toList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {δ : Type w}
  {m : Type w → Type w'} [inst : Std.TransCmp cmp] [inst_1 : Monad m] [inst_2 : LawfulMonad m]
  {f : δ → (a : α) → β a → m δ} {init : δ},
  Std.ExtDTreeMap.foldlM f init t = List.foldlM (fun a b => f a b.fst b.snd) init t.toList
-- Mathlib.Data.W.Basic
WType.mk.sizeOf_spec : ∀ {α : Type u_1} {β : α → Type u_2} [inst : SizeOf α] [inst_1 : (a : α) → SizeOf (β a)] (a : α) (f : β a → WType β),
  sizeOf (WType.mk a f) = 1 + sizeOf a
-- Mathlib.CategoryTheory.FiberedCategory.Fibered
CategoryTheory.Functor.IsFibered.mk : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} [toIsPreFibered : p.IsPreFibered],
  (∀ {R S T : 𝒮} (f : R ⟶ S) (g : S ⟶ T) {a b c : 𝒳} (φ : a ⟶ b) (ψ : b ⟶ c) [p.IsCartesian f φ] [p.IsCartesian g ψ],
      p.IsCartesian (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp φ ψ)) →
    p.IsFibered
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.optionEquivalence_inverse : ∀ {J : Type w₁} (C' : Option J → Type u₁) [inst : (i : Option J) → CategoryTheory.Category.{v₁, u₁} (C' i)],
  (CategoryTheory.Pi.optionEquivalence C').inverse =
    CategoryTheory.Functor.pi' fun i =>
      match i with
      | none => CategoryTheory.Prod.fst (C' none) ((j : J) → C' (some j))
      | some i =>
        (CategoryTheory.Prod.snd (C' none) ((j : J) → C' (some j))).comp
          (CategoryTheory.Pi.eval (fun j => C' (some j)) i)
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.instFiniteOfIsNoetherian : ∀ {A : Type u_6} {G : Type u_7} {V : Type u_8} {W : Type u_9} [inst : CommRing A] [inst_1 : Monoid G]
  [inst_2 : AddCommGroup V] [inst_3 : AddCommGroup W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W) [Module.Finite A V] [IsNoetherian A W],
  Module.Finite A (ρ.IntertwiningMap σ)
-- Init.Data.SInt.Lemmas
ISize.ofBitVec_ofNatLT : ∀ (n : ℕ) (hn : n < 2 ^ System.Platform.numBits), ISize.ofBitVec n#'hn = ISize.ofNat n
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.IsSymm.neg : ∀ {R₁ : Type u_3} {M₁ : Type u_4} [inst : CommRing R₁] [inst_1 : AddCommGroup M₁] [inst_2 : Module R₁ M₁]
  {B : LinearMap.BilinForm R₁ M₁}, B.IsSymm → (-B).IsSymm
-- Mathlib.Analysis.Normed.Field.Basic
DenselyNormedField.mk : {α : Type u_5} →
  [toNormedField : NormedField α] → (∀ (x y : ℝ), 0 ≤ x → x < y → ∃ a, x < ‖a‖ ∧ ‖a‖ < y) → DenselyNormedField α
-- Mathlib.Analysis.Normed.Group.Bounded
/-- In a (semi)normed group, negation `x ↦ -x` tends to infinity at infinity.  -/
Filter.tendsto_neg_cobounded : ∀ {E : Type u_2} [inst : SeminormedAddGroup E], Filter.Tendsto Neg.neg (Bornology.cobounded E) (Bornology.cobounded E)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get_union_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (mem : k ∈ m₂),
  Std.DHashMap.Raw.Const.get (m₁ ∪ m₂) k ⋯ = Std.DHashMap.Raw.Const.get m₂ k mem
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.mkAppS₄ : {m : Type → Type} →
  [Lean.Meta.Sym.Internal.MonadShareCommon m] →
    [Monad m] → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.darts_concat : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (h : G.Adj v w),
  (p.concat h).darts = p.darts.concat { fst := v, snd := w, adj := h }
-- Mathlib.Combinatorics.Additive.Energy
Finset.mulEnergy_pos : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Mul α] {s t : Finset α}, s.Nonempty → t.Nonempty → 0 < s.mulEnergy t
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.map_id : ∀ {α : Type u_1} [inst : TopologicalSpace α] (K : TopologicalSpace.CompactOpens α),
  TopologicalSpace.CompactOpens.map id ⋯ ⋯ K = K
-- Mathlib.Topology.Algebra.Group.Basic
neg_mem_connectedComponent_zero : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : SubtractionMonoid G] [ContinuousNeg G] {g : G},
  g ∈ connectedComponent 0 → -g ∈ connectedComponent 0
-- Mathlib.Analysis.Convex.Star
/-- Star-convexity of sets. `s` is star-convex at `x` if every segment from `x` to a point in `s` is
contained in `s`.  -/
StarConvex : (𝕜 : Type u_4) → {E : Type u_5} → [Semiring 𝕜] → [PartialOrder 𝕜] → [AddCommMonoid E] → [SMul 𝕜 E] → E → Set E → Prop
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
/-- Two equivalent open partial homeomorphisms have coinciding `toFun` on the source  -/
OpenPartialHomeomorph.EqOnSource.eqOn : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e e' : OpenPartialHomeomorph X Y}, e ≈ e' → Set.EqOn (↑e) (↑e') e.source
-- Init.Data.Int.Lemmas
Int.instLawfulIdentityHMulOfNat : Std.LawfulIdentity (fun x1 x2 => x1 * x2) 1
-- Mathlib.LinearAlgebra.Matrix.WithConv
Matrix.toLin'_hadamard : ∀ {m : Type u_1} {n : Type u_2} {α : Type u_3} [inst : CommSemiring α] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  (x y : Matrix m n α),
  Matrix.toLin' (x.hadamard y) = (WithConv.toConv (Matrix.toLin' x) * WithConv.toConv (Matrix.toLin' y)).ofConv
-- Init.Data.List.MapIdx
List.mapIdx_eq_append_iff : ∀ {α : Type u_1} {α_1 : Type u_2} {f : ℕ → α → α_1} {l₁ l₂ : List α_1} {l : List α},
  List.mapIdx f l = l₁ ++ l₂ ↔
    ∃ l₁' l₂', l = l₁' ++ l₂' ∧ List.mapIdx f l₁' = l₁ ∧ List.mapIdx (fun i => f (i + l₁'.length)) l₂' = l₂
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsLoop.mem_ground : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsLoop e → e ∈ M.E
-- Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Besicovitch.SatelliteConfig.exists_normalized_aux1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {N : ℕ} {τ : ℝ} (a : Besicovitch.SatelliteConfig E N τ),
  a.r (Fin.last N) = 1 →
    1 ≤ τ → ∀ (δ : ℝ), τ ≤ 1 + δ / 4 → δ ≤ 1 → ∀ (i j : Fin N.succ), i ≠ j → 1 - δ ≤ ‖a.c i - a.c j‖
-- Mathlib.Topology.Homotopy.Equiv
ContinuousMap.HomotopyEquiv.coe_invFun : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (h : ContinuousMap.HomotopyEquiv X Y), ⇑h.invFun = ⇑h.symm.toFun
-- Mathlib.Algebra.Ring.Opposite
MulOpposite.unop_natCast : ∀ {R : Type u_1} [inst : NatCast R] (n : ℕ), MulOpposite.unop ↑n = ↑n
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_eq_getD_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α} {fallback : β},
  Std.ExtDHashMap.Const.getD m a fallback = (Std.ExtDHashMap.Const.get? m a).getD fallback
-- Mathlib.NumberTheory.ModularForms.Derivative
/-- As a corollary, if `F` is invariant under the slash action of weight `k`, then
`serreDerivative k F` is invariant under the slash action of weight `k + 2`.
 -/
Derivative.serreDerivative_slash_invariant : ∀ {k : ℤ} {F : UpperHalfPlane → ℂ},
  MDiff F →
    ∀ {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ},
      SlashAction.map k γ F = F →
        SlashAction.map (k + 2) γ (Derivative.serreDerivative (↑k) F) = Derivative.serreDerivative (↑k) F
-- Mathlib.Algebra.Notation.Support
Function.support_comp_subset : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : Zero M] [inst_1 : Zero N] {g : M → N},
  g 0 = 0 → ∀ (f : ι → M), Function.support (g ∘ f) ⊆ Function.support f
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.stepNormal.eq_2 : Turing.ToPartrec.stepNormal Turing.ToPartrec.Code.succ = fun k v => Turing.ToPartrec.Cfg.ret k [v.headI.succ]
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.sum.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [inst : Countable ι]
  (κ κ_1 : ι → ProbabilityTheory.Kernel α β),
  κ = κ_1 → ProbabilityTheory.Kernel.sum κ = ProbabilityTheory.Kernel.sum κ_1
-- Init.Data.Int.Lemmas
Int.ofNat_ne_zero : ∀ {n : ℕ}, ↑n ≠ 0 ↔ n ≠ 0
-- Mathlib.Topology.Separation.Regular
exists_nhds_disjoint_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T25Space X] {x y : X},
  x ≠ y → ∃ s ∈ nhds x, ∃ t ∈ nhds y, Disjoint (closure s) (closure t)
-- Mathlib.RingTheory.LocalRing.ResidueField.Fiber
PrimeSpectrum.coe_preimageOrderIsoFiber_symm_apply_coe_asIdeal : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : PrimeSpectrum R)
  (q : PrimeSpectrum (p.asIdeal.Fiber S)),
  ↑(↑((RelIso.symm (PrimeSpectrum.preimageOrderIsoFiber R S p)) q)).asIdeal =
    ⇑Algebra.TensorProduct.includeRight ⁻¹' ↑q.asIdeal
-- Mathlib.Analysis.Normed.Ring.InfiniteSum
Summable.mul_of_nonneg : ∀ {ι : Type u_2} {ι' : Type u_3} {f : ι → ℝ} {g : ι' → ℝ},
  Summable f → Summable g → 0 ≤ f → 0 ≤ g → Summable fun x => f x.1 * g x.2
-- Init.Data.Int.Linear
Int.Internal.Linear.le_eq_true : ∀ (ctx : Int.Internal.Linear.Context) (lhs rhs : Int.Internal.Linear.Expr),
  (lhs.sub rhs).norm.isValidLe = true →
    (Int.Internal.Linear.Expr.denote ctx lhs ≤ Int.Internal.Linear.Expr.denote ctx rhs) = True
-- Mathlib.Algebra.Order.Ring.Int
Int.two_le_iff_pos_of_even : ∀ {m : ℤ}, Even m → (2 ≤ m ↔ 0 < m)
-- Mathlib.CategoryTheory.Category.Basic
CategoryTheory.CategoryStruct.toQuiver : {obj : Type u} → [self : CategoryTheory.CategoryStruct.{v, u} obj] → Quiver obj