mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_filter_not_contains_map_fst : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    ∀ {h₁ : Std.Internal.List.containsKey k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) = true}
      {h₂ : Std.Internal.List.containsKey k l₁ = true},
      Std.Internal.List.getKey k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) h₁ =
        Std.Internal.List.getKey k l₁ h₂
-- Mathlib.GroupTheory.Congruence.Defs
/-- Two elements are related by a congruence relation `c` iff they are represented by the same
element of the quotient by `c`.  -/
Con.eq : ∀ {M : Type u_1} [inst : Mul M] (c : Con M) {a b : M}, ↑a = ↑b ↔ c a b
-- Mathlib.Order.Filter.Extr
IsMaxFilter.comp_mono : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {l : Filter α} {a : α},
  IsMaxFilter f l a → ∀ {g : β → γ}, Monotone g → IsMaxFilter (g ∘ f) l a
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
/-- Induction on the completion of a number field at an infinite place: a closed property that
holds on the image of `K` holds everywhere.  -/
NumberField.InfinitePlace.Completion.induction_on : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K) {p : v.Completion → Prop} (x : v.Completion),
  IsClosed {x | p x} → (∀ (a : WithAbs ↑v), p { toCompletion := ↑a }) → p x
-- Lean.Meta.Basic
/-- Eta for structures configuration mode.  -/
Lean.Meta.Config.etaStruct : Lean.Meta.Config → Lean.Meta.EtaStructMode
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map_add_le : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  {x y : R} {g : Γ₀}, v x ≤ g → v y ≤ g → v (x + y) ≤ g
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstrProof.core.sizeOf_spec : ∀ (a b : Lean.Expr) (lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr),
  sizeOf (Lean.Meta.Grind.Arith.Linear.EqCnstrProof.core a b lhs rhs) =
    1 + sizeOf a + sizeOf b + sizeOf lhs + sizeOf rhs
-- Mathlib.Analysis.Normed.Group.BallSphere
coe_neg_sphere : ∀ {E : Type u_1} [i : SeminormedAddCommGroup E] {r : ℝ} (v : ↑(Metric.sphere 0 r)), ↑(-v) = -↑v
-- Mathlib.Algebra.Category.Grp.Basic
/-- **Alias** of `CategoryTheory.ConcreteCategory.forget_map_eq_ofHom`. -/
CommGrpCat.forget_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)}
  {CC : outParam (C → Type w)} [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))]
  [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.forget C).map f = TypeCat.ofHom ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.IsSeparated.mk : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  autoParam (AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Limits.pullback.diagonal f))
      AlgebraicGeometry.IsSeparated.isClosedImmersion_diagonal._autoParam →
    AlgebraicGeometry.IsSeparated f
-- Mathlib.Analysis.Convex.StrictConvexSpace
/-- A *strictly convex space* is a normed space where the closed balls are strictly convex. We only
require balls of positive radius with center at the origin to be strictly convex in the definition,
then prove that any closed ball is strictly convex in `strictConvex_closedBall` below.

See also `StrictConvexSpace.of_strictConvex_unitClosedBall`.  -/
StrictConvexSpace : (𝕜 : Type u_1) →
  (E : Type u_2) →
    [inst : NormedField 𝕜] → [PartialOrder 𝕜] → [inst_2 : NormedAddCommGroup E] → [NormedSpace 𝕜 E] → Prop
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.C_ne_zero : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonAssocSemiring R] {r : R}, r ≠ 0 → HahnSeries.C r ≠ 0
-- Mathlib.Topology.Separation.Hausdorff
/-- In a `T2Space X`, for a compact set `t` and a point `x` outside `t`, there are open sets `U`,
`V` that separate `t` and `x`.  -/
IsCompact.separation_of_notMem : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] {x : X} {t : Set X},
  IsCompact t → x ∉ t → ∃ U V, IsOpen U ∧ IsOpen V ∧ t ⊆ U ∧ x ∈ V ∧ Disjoint U V
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.op_injective : ∀ {M : Type u_2} [inst : AddZeroClass M], Function.Injective AddSubmonoid.op
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.FinMeasSupp.pair : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} [inst : Zero β] [inst_1 : Zero γ]
  {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α β} {g : MeasureTheory.SimpleFunc α γ},
  f.FinMeasSupp μ → g.FinMeasSupp μ → (f.pair g).FinMeasSupp μ
-- Mathlib.Order.Extension.Well
toWellOrderExtension_strictMono : ∀ {α : Type u} [inst : Preorder α] [inst_1 : WellFoundedLT α], StrictMono ⇑toWellOrderExtension
-- Mathlib.Order.Bounds.Basic
BddBelow.dual : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, BddBelow s → BddAbove (⇑OrderDual.ofDual ⁻¹' s)
-- Mathlib.Algebra.Category.Grp.FilteredColimits
AddGrpCat.FilteredColimits.colimitNeg.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J AddGrpCat),
  AddGrpCat.FilteredColimits.colimitNeg F =
    { neg := fun x => Quot.lift (AddGrpCat.FilteredColimits.colimitNegAux F) ⋯ x }
-- Mathlib.CategoryTheory.ObjectProperty.Basic
/-- The property of objects in a category that is satisfied by `X : C` and `Y : C`.  -/
CategoryTheory.ObjectProperty.pair : {C : Type u} → [inst : CategoryTheory.CategoryStruct.{v, u} C] → C → C → CategoryTheory.ObjectProperty C
-- Init.Data.List.Lemmas
List.get_mk_zero : ∀ {α : Type u_1} {l : List α} (h : 0 < l.length), l.get ⟨0, h⟩ = l.head ⋯
-- Mathlib.CategoryTheory.Functor.Const
/-- The constant functor `Jᵒᵖ ⥤ Cᵒᵖ` sending everything to `op X`
is (naturally isomorphic to) the opposite of the constant functor `J ⥤ C` sending everything to `X`.
 -/
CategoryTheory.Functor.const.opObjOp : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C] →
        (X : C) → (CategoryTheory.Functor.const Jᵒᵖ).obj (Opposite.op X) ≅ ((CategoryTheory.Functor.const J).obj X).op
-- Mathlib.Data.Multiset.AddSub
Multiset.coe_erase : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (a : α), (↑l).erase a = ↑(l.erase a)
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.MonoidalCategory.associator_naturality : ∀ {R : Type u} [inst : CommSemiring R] {X₁ : SemimoduleCat R} {X₂ : SemimoduleCat R} {X₃ : SemimoduleCat R}
  {Y₁ : SemimoduleCat R} {Y₂ : SemimoduleCat R} {Y₃ : SemimoduleCat R} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
  CategoryTheory.CategoryStruct.comp
      (SemimoduleCat.MonoidalCategory.tensorHom (SemimoduleCat.MonoidalCategory.tensorHom f₁ f₂) f₃)
      (SemimoduleCat.MonoidalCategory.associator Y₁ Y₂ Y₃).hom =
    CategoryTheory.CategoryStruct.comp (SemimoduleCat.MonoidalCategory.associator X₁ X₂ X₃).hom
      (SemimoduleCat.MonoidalCategory.tensorHom f₁ (SemimoduleCat.MonoidalCategory.tensorHom f₂ f₃))
-- Init.Data.String.Lemmas.Iter
_private.Init.Data.String.Lemmas.Iter.0.Std.Iter.intercalateString.match_1.eq_2 : ∀ (motive : Option String → String → Sort u_1) (str sl : String) (h_1 : (sl : String) → motive none sl)
  (h_2 : (str sl : String) → motive (some str) sl),
  (match some str, sl with
    | none, sl => h_1 sl
    | some str, sl => h_2 str sl) =
    h_2 str sl
-- Mathlib.Data.List.TakeDrop
List.takeI_eq_take : ∀ {α : Type u} [inst : Inhabited α] {n : ℕ} {l : List α}, n ≤ l.length → List.takeI n l = List.take n l
-- Mathlib.Analysis.Distribution.TestFunction
/-- The type of bundled `n`-times continuously differentiable maps with compact support  -/
TestFunction : {E : Type u_3} →
  [inst : NormedAddCommGroup E] →
    [NormedSpace ℝ E] →
      TopologicalSpace.Opens E →
        (F : Type u_4) → [inst : NormedAddCommGroup F] → [NormedSpace ℝ F] → ℕ∞ → Type (max u_3 u_4)
-- Lean.DocString.Formatter
_private.Lean.DocString.Formatter.0.Lean.Doc.Parser.versoSyntaxToString'.startBlock : ReaderT ℕ (StateM String) Unit
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.trNormal.eq_1 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (k : K) (a : σ → Γ k) (q : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2to1.trNormal (Turing.TM2.Stmt.push k a q) =
    Turing.TM1.Stmt.goto fun x x_1 => Turing.TM2to1.Λ'.go k (Turing.TM2to1.StAct.push a) q
-- Mathlib.Topology.UniformSpace.Basic
IsOpen.relPreimage : ∀ {α : Type ua} {β : Type ub} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : SetRel α β},
  IsOpen s → ∀ {t : Set β}, IsOpen (s.preimage t)
-- Mathlib.Data.WSeq.Basic
_private.Mathlib.Data.WSeq.Basic.0.Stream'.Seq.omap.match_1.eq_1 : ∀ {α : Type u_2} {β : Type u_1} (motive : Option (α × β) → Sort u_3) (h_1 : Unit → motive none)
  (h_2 : (a : α) → (b : β) → motive (some (a, b))),
  (match none with
    | none => h_1 ()
    | some (a, b) => h_2 a b) =
    h_1 ()
-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.Scheme.affineOpenCover_idx : ∀ (X : AlgebraicGeometry.Scheme) (x : ↥X), X.affineOpenCover.idx x = ⋯.choose
-- Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
/-- In a concrete category `C`, given two morphisms `f₁ : X₁ ⟶ S` and `f₂ : X₂ ⟶ S`,
the elements in `pullback f₁ f₂` can be identified to compatible tuples of
elements in `X₁` and `X₂`.  -/
CategoryTheory.Limits.Concrete.pullbackEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : C → C → Type u_1} →
      {CC : C → Type v} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory C FC] →
            {X₁ X₂ S : C} →
              (f₁ : X₁ ⟶ S) →
                (f₂ : X₂ ⟶ S) →
                  [inst_3 : CategoryTheory.Limits.HasPullback f₁ f₂] →
                    [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f₁ f₂)
                          (CategoryTheory.forget C)] →
                      CategoryTheory.ToType (CategoryTheory.Limits.pullback f₁ f₂) ≃
                        { p //
                          (CategoryTheory.ConcreteCategory.hom f₁) p.1 = (CategoryTheory.ConcreteCategory.hom f₂) p.2 }
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.isOpen_extend_preimage : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {s : Set E},
  IsOpen s → IsOpen (f.source ∩ ↑(f.extend I) ⁻¹' s)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
/-- An integrability criterion for the continuous functional calculus.
This version assumes joint continuity of `f`, see `integrableOn_cfc'` for a statement
with weaker assumptions.  -/
integrableOn_cfc : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : MeasurableSpace X]
  {μ : MeasureTheory.Measure X} [inst_2 : NormedRing A] [inst_3 : StarRing A] [inst_4 : NormedAlgebra 𝕜 A]
  [inst_5 : ContinuousFunctionalCalculus 𝕜 A p] [CompleteSpace A] [inst_7 : TopologicalSpace X] [OpensMeasurableSpace X]
  {s : Set X},
  MeasurableSet s →
    ∀ (f : X → 𝕜 → 𝕜) (bound : X → ℝ) (a : A) [SecondCountableTopologyEither X C(↑(spectrum 𝕜 a), 𝕜)],
      ContinuousOn (Function.uncurry f) (s ×ˢ spectrum 𝕜 a) →
        (∀ᵐ (x : X) ∂μ.restrict s, ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ bound x) →
          MeasureTheory.HasFiniteIntegral bound (μ.restrict s) →
            autoParam (p a) integrableOn_cfc._auto_1 → MeasureTheory.IntegrableOn (fun x => cfc (f x) a) s μ
-- Mathlib.RingTheory.Trace.Quotient
RingHom.quotientKerEquivOfRightInverse.congr_simp : ∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Semiring S] {f : R →+* S} {g g_1 : S → R} (e_g : g = g_1)
  (hf : Function.RightInverse g ⇑f),
  RingHom.quotientKerEquivOfRightInverse hf = RingHom.quotientKerEquivOfRightInverse ⋯
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_diff_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α], m₁.WF → m₂.WF → ∀ {k : α} [inst_3 : Inhabited (β k)], k ∉ m₂ → (m₁ \ m₂).get! k = m₁.get! k
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- `LinearMap.toAddMonoidHom` promoted to an `AddMonoidHom`.  -/
LinearMap.toAddMonoidHom' : {R₁ : Type u_2} →
  {R₂ : Type u_3} →
    {M : Type u_8} →
      {M₂ : Type u_10} →
        [inst : Semiring R₁] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R₁ M] → [inst_5 : Module R₂ M₂] → {σ₁₂ : R₁ →+* R₂} → (M →ₛₗ[σ₁₂] M₂) →+ M →+ M₂
-- Aesop.Script.SpecificTactics
Aesop.Script.TacticBuilder.replace : Lean.MVarId → Lean.MVarId → Lean.FVarId → Lean.Expr → Lean.Expr → Aesop.Script.TacticBuilder
-- Std.Internal.Do.PredTrans
Std.Internal.Do.PredTrans.ext_iff : ∀ {Pred : Type u_1} {EPred : Type u_2} {α : Type u_3} {x y : Std.Internal.Do.PredTrans Pred EPred α},
  x = y ↔ ∀ (post : α → Pred) (epost : EPred), x.apply post epost = y.apply post epost
-- Aesop.Index.Basic
Aesop.instInhabitedIndexMatchResult : {a : Type} → [Inhabited a] → Inhabited (Aesop.IndexMatchResult a)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.nonDegenerate₂ : ∀ {X : SSet} {A : X.Subcomplex} (self : A.PairingCore) (s : self.ι),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X (self.index s))) (self.simplex s) ∈
    X.nonDegenerate (self.dim s)
-- Mathlib.GroupTheory.Coset.Basic
Subgroup.quotientiInfEmbedding.eq_1 : ∀ {α : Type u_1} [inst : Group α] {ι : Type u_2} (f : ι → Subgroup α),
  Subgroup.quotientiInfEmbedding f = { toFun := fun q i => Subgroup.quotientMapOfLE ⋯ q, inj' := ⋯ }
-- Mathlib.Testing.Plausible.Functions
Plausible.InjectiveFunction.mapToSelf.inj : ∀ {α : Type u} {xs : List ((_ : α) × α)} {a : (List.map Sigma.fst xs).Perm (List.map Sigma.snd xs)}
  {a_1 : (List.map Sigma.snd xs).Nodup} {xs_1 : List ((_ : α) × α)}
  {a_2 : (List.map Sigma.fst xs_1).Perm (List.map Sigma.snd xs_1)} {a_3 : (List.map Sigma.snd xs_1).Nodup},
  Plausible.InjectiveFunction.mapToSelf xs a a_1 = Plausible.InjectiveFunction.mapToSelf xs_1 a_2 a_3 → xs = xs_1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_congr : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k k' : α}, cmp k k' = Ordering.eq → (k ∈ t ↔ k' ∈ t)
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
/-- Auxiliary definition for `HasCokernels SemiNormedGrp₁`.  -/
SemiNormedGrp₁.cokernelCocone : {X Y : SemiNormedGrp₁} → (f : X ⟶ Y) → CategoryTheory.Limits.Cofork f 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_diff_of_contains_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Inhabited α]
  [Std.TransOrd α] (h₁ : m₁.WF),
  m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₂ = true → (m₁.diff m₂ ⋯).getKey! k = default
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey?_unitOfList_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k : α},
  l.contains k = false → (Std.DHashMap.Raw.Const.unitOfList l).getKey? k = none
-- Mathlib.Data.Fintype.Order
le_sSup_iff_of_directedOn : ∀ {α : Type u_2} [inst : CompleteLattice α] {s : Set α} {a : α},
  s.Nonempty → s.Finite → DirectedOn (fun x1 x2 => x1 ≤ x2) s → (a ≤ sSup s ↔ ∃ b ∈ s, a ≤ b)
-- Init.Data.String.Bootstrap
Substring.Raw.Internal.isEmpty : Substring.Raw → Bool
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
/-- The derivative of `riemannZeta` at `s = 0` equals `-log(2π) / 2`.  -/
deriv_riemannZeta_zero : deriv riemannZeta 0 = -Complex.log (2 * ↑Real.pi) / 2
-- Mathlib.Data.Finset.Powerset
Finset.powerset_card_biUnion : ∀ {α : Type u_1} [inst : DecidableEq (Finset α)] (s : Finset α),
  s.powerset = (Finset.range (s.card + 1)).biUnion fun i => Finset.powersetCard i s
-- Mathlib.Algebra.Polynomial.DenomsClearable
/-- If `i : R → K` is a ring homomorphism, `f` is a polynomial with coefficients in `R`,
`a, b` are elements of `R`, with `i b` invertible, then there is a `D ∈ R` such that
`b ^ f.natDegree * f (a / b)` equals `i D`.  -/
denomsClearable_natDegree : ∀ {R : Type u_1} {K : Type u_2} [inst : Semiring R] [inst_1 : CommSemiring K] {b : R} {bi : K} (i : R →+* K)
  (f : Polynomial R) (a : R), bi * i b = 1 → DenomsClearable a b f.natDegree f i
-- Mathlib.Analysis.Normed.Group.Pointwise
singleton_sub_sphere : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x y : E), {x} - Metric.sphere y δ = Metric.sphere (x - y) δ
-- Init.Data.Bool
Bool.ne_of_lt : ∀ {x y : Bool}, x < y → x ≠ y
-- Mathlib.Analysis.Convex.Strong
StrongConcaveOn.mono : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E} {f : E → ℝ} {m n : ℝ},
  m ≤ n → StrongConcaveOn s n f → StrongConcaveOn s m f
-- Lean.Meta.Tactic.Cases
Lean.Meta.Cases.Context.mk.injEq : ∀ (inductiveVal : Lean.InductiveVal) (nminors : ℕ) (majorDecl : Lean.LocalDecl) (majorTypeFn : Lean.Expr)
  (majorTypeArgs majorTypeIndices : Array Lean.Expr) (inductiveVal_1 : Lean.InductiveVal) (nminors_1 : ℕ)
  (majorDecl_1 : Lean.LocalDecl) (majorTypeFn_1 : Lean.Expr) (majorTypeArgs_1 majorTypeIndices_1 : Array Lean.Expr),
  ({ inductiveVal := inductiveVal, nminors := nminors, majorDecl := majorDecl, majorTypeFn := majorTypeFn,
        majorTypeArgs := majorTypeArgs, majorTypeIndices := majorTypeIndices } =
      { inductiveVal := inductiveVal_1, nminors := nminors_1, majorDecl := majorDecl_1, majorTypeFn := majorTypeFn_1,
        majorTypeArgs := majorTypeArgs_1, majorTypeIndices := majorTypeIndices_1 }) =
    (inductiveVal = inductiveVal_1 ∧
      nminors = nminors_1 ∧
        majorDecl = majorDecl_1 ∧
          majorTypeFn = majorTypeFn_1 ∧ majorTypeArgs = majorTypeArgs_1 ∧ majorTypeIndices = majorTypeIndices_1)
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.compr₂ₛₗ_id : ∀ {R : Type u_2} [inst : CommSemiring R] {R₂ : Type u_14} {R₃ : Type u_15} {M : Type u_17} {N : Type u_18}
  {P : Type u_19} [inst_1 : CommSemiring R₂] [inst_2 : CommSemiring R₃] [inst_3 : AddCommMonoid M]
  [inst_4 : AddCommMonoid N] [inst_5 : AddCommMonoid P] [inst_6 : Module R M] [inst_7 : Module R₂ N]
  [inst_8 : Module R₃ P] {σ₁₃ : R →+* R₃} {σ₂₃ : R₂ →+* R₃} (f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P), f.compr₂ₛₗ LinearMap.id = f
-- Init.Grind.AC
Lean.Grind.AC.instBEqSeq.beq.eq_def : ∀ (x x_1 : Lean.Grind.AC.Seq),
  Lean.Grind.AC.instBEqSeq.beq x x_1 =
    match x, x_1 with
    | Lean.Grind.AC.Seq.var a, Lean.Grind.AC.Seq.var b => a == b
    | Lean.Grind.AC.Seq.cons a a_1, Lean.Grind.AC.Seq.cons b b_1 => a == b && Lean.Grind.AC.instBEqSeq.beq a_1 b_1
    | x, x_2 => false
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfcHom_isStrictlyPositive_iff : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [ContinuousSqrt R]
  [StarOrderedRing R] [inst_8 : TopologicalSpace A] [inst_9 : Ring A] [inst_10 : StarRing A] [inst_11 : PartialOrder A]
  [StarOrderedRing A] [inst_13 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A]
  {a : A} (ha : p a) {f : C(↑(spectrum R a), R)}, IsStrictlyPositive ((cfcHom ha) f) ↔ ∀ (x : ↑(spectrum R a)), 0 < f x
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.MeasurePreserving.mk : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : α → β}
  {μa : autoParam (MeasureTheory.Measure α) MeasureTheory.MeasurePreserving._auto_1}
  {μb : autoParam (MeasureTheory.Measure β) MeasureTheory.MeasurePreserving._auto_3},
  Measurable f → MeasureTheory.Measure.map f μa = μb → MeasureTheory.MeasurePreserving f μa μb
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.isScalarTower_self : ∀ {R : Type u_1} (S : Type u_2) {M : Type u_3} [inst : Semiring S] [inst_1 : DistribSMul R S] [inst_2 : Mul M]
  [IsScalarTower R S S], IsScalarTower R (MonoidAlgebra S M) (MonoidAlgebra S M)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.support_pow_succ : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (n : ℕ), (I ^ (n + 1)).support = I.support
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.coe_codRestrict_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (f : A →A[R] B) (p : Subalgebra R B) (h : ∀ (x : A), f x ∈ p) (x : A), ↑((f.codRestrict p h) x) = f x
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
AlgebraicTopology.DoldKan.PInfty_comp_QInfty_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} {Z : ChainComplex C ℕ}
  (h : AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty
      (CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.QInfty h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Std.Data.DHashMap.IteratorLemmas
Std.DHashMap.Raw.toArray_keysIter : ∀ {α : Type u} {β : α → Type u} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → m.keysIter.toArray = m.keysArray
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.BundledIterM.Equiv.trans : ∀ {m : Type w → Type w'} {β : Type w} [inst : Monad m] [inst_1 : LawfulMonad m] {ita itb itc : Std.BundledIterM m β},
  Std.BundledIterM.Equiv m β ita itb → Std.BundledIterM.Equiv m β itb itc → Std.BundledIterM.Equiv m β ita itc
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Real.tan_eq_zero_iff' : ∀ {θ : ℝ}, Real.cos θ ≠ 0 → (Real.tan θ = 0 ↔ ∃ k, ↑k * Real.pi = θ)
-- Mathlib.Algebra.Group.End
AddAut.addConj_neg_apply : ∀ {G : Type u_3} [inst : AddGroup G] (g h : G), (-AddAut.addConj g) h = -g + h + g
-- Batteries.Data.Array.Scan
/-- ### Array.scanl  -/
Array.scanl_eq_scanlM : ∀ {β : Type u_1} {α : Type u_2} {init : β} {f : β → α → β} {as : Array α},
  Array.scanl f init as = (Array.scanlM (fun x1 x2 => pure (f x1 x2)) init as).run
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
/-- The explicit pullback cone of `X, Y` given by `{ p : X × Y // f p.1 = g p.2 }`.  -/
TopCat.pullbackCone : {X Y Z : TopCat} → (f : X ⟶ Z) → (g : Y ⟶ Z) → CategoryTheory.Limits.PullbackCone f g
-- Mathlib.Order.Filter.Extr
/-- If `f` is antitone on `Icc a b` and monotone on `Ico b c`, then the minimum of `f` on
`Ico a c` is attained at `b`.  -/
isMinOn_Ico_of_anti_mono : ∀ {α : Type u} {β : Type u_1} [inst : LinearOrder α] [inst_1 : Preorder β] {a b c : α} {f : α → β},
  AntitoneOn f (Set.Icc a b) → MonotoneOn f (Set.Ico b c) → IsMinOn f (Set.Ico a c) b
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bsup_succ_le_blsub : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}),
  Order.succ (o.bsup f) ≤ o.blsub f ↔ ∃ i, ∃ (hi : i < o), f i hi = o.bsup f
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.IsDominant.mk : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y}, DenseRange ⇑f → AlgebraicGeometry.IsDominant f