mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {f : α → β → γ} {k : α} {fallback : γ},
  t.WF → (Std.TreeMap.Raw.map f t).getD k fallback = (Option.map (f k) t[k]?).getD fallback
-- Mathlib.LinearAlgebra.AffineSpace.Combination
Finset.sum_weightedVSubVSubWeights : ∀ (k : Type u_1) [inst : Ring k] {ι : Type u_4} (s : Finset ι) [inst_1 : DecidableEq ι] {i j : ι},
  i ∈ s → j ∈ s → ∑ t ∈ s, Finset.weightedVSubVSubWeights k i j t = 0
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly_nc : Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Poly
-- Lean.Util.NumApps
Lean.Expr.NumApps.M : Type → Type
-- Mathlib.Analysis.InnerProductSpace.Calculus
HasDerivAt.norm_sq : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {f : ℝ → F} {f' : F} {x : ℝ},
  HasDerivAt f f' x → HasDerivAt (fun x => ‖f x‖ ^ 2) (2 * inner ℝ (f x) f') x
-- Mathlib.CategoryTheory.Monad.Monadicity
CategoryTheory.Monad.instHasCoequalizerMapAAppCounitObjAOfHasCoequalizerOfIsSplitPair : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G)
  [CategoryTheory.Monad.HasCoequalizerOfIsSplitPair G] (A : adj.toMonad.Algebra),
  CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.sup_apply : ∀ {α : Type u_1} (m₁ m₂ : MeasureTheory.OuterMeasure α) (s : Set α), (m₁ ⊔ m₂) s = max (m₁ s) (m₂ s)
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
/-- A set of `ℕ` is semilinear if and only if it is ultimately periodic, i.e. periodic after some
number `k`.  -/
Nat.isSemilinearSet_iff_ultimately_periodic : ∀ {s : Set ℕ}, IsSemilinearSet s ↔ ∃ k, ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinitesimal_epsilon : Hyperreal.epsilon.Infinitesimal
-- Mathlib.NumberTheory.Padics.PadicVal.Defs
/-- A simplification of `padicValNat` when one input is prime, by analogy with
`padicValRat_def`.  -/
padicValNat_def : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ}, n ≠ 0 → padicValNat p n = multiplicity p n
-- Mathlib.Data.Nat.Cast.Commute
Commute.natCast_mul_left : ∀ {α : Type u_1} [inst : Semiring α] {a b : α}, Commute a b → ∀ (n : ℕ), Commute (↑n * a) b
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.instEpiπ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z), CategoryTheory.Epi (CategoryTheory.kernelCokernelCompSequence.π f g)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.forM_eq_forM_toArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : (a : α) × β a → m PUnit.{w + 1}}, forM t f = forM t.toArray f
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.singleton_dep : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.Dep {e} ↔ M.IsLoop e
-- Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
continuousWithinAt_continuousAlternatingMap_bundle : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : Fintype ι] {B : Type u_3}
  [inst_2 : TopologicalSpace B] {F₁ : Type u_4} [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁]
  {E₁ : B → Type u_5} [inst_5 : (x : B) → AddCommGroup (E₁ x)] [inst_6 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_7 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [inst_8 : (x : B) → TopologicalSpace (E₁ x)]
  [inst_9 : FiberBundle F₁ E₁] [inst_10 : VectorBundle 𝕜 F₁ E₁] {F₂ : Type u_6} [inst_11 : NormedAddCommGroup F₂]
  [inst_12 : NormedSpace 𝕜 F₂] {E₂ : B → Type u_7} [inst_13 : (x : B) → AddCommGroup (E₂ x)]
  [inst_14 : (x : B) → Module 𝕜 (E₂ x)] [inst_15 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_16 : (x : B) → TopologicalSpace (E₂ x)] [inst_17 : FiberBundle F₂ E₂] [inst_18 : VectorBundle 𝕜 F₂ E₂]
  [inst_19 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)] [inst_20 : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] {X : Type u_8}
  [inst_21 : TopologicalSpace X] {s : Set X} {x₀ : X}
  (f : X → Bundle.TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun x => E₁ x [⋀^ι]→L[𝕜] E₂ x),
  ContinuousWithinAt f s x₀ ↔
    ContinuousWithinAt (fun x => (f x).proj) s x₀ ∧
      ContinuousWithinAt
        (fun x => ContinuousAlternatingMap.inCoordinates F₁ F₂ (f x₀).proj (f x).proj (f x₀).proj (f x).proj (f x).snd)
        s x₀
-- Mathlib.RingTheory.Kaehler.Polynomial
KaehlerDifferential.mvPolynomialBasis_repr_D_X : ∀ (R : Type u) [inst : CommRing R] (σ : Type u_1) (i : σ),
  (KaehlerDifferential.mvPolynomialBasis R σ).repr ((KaehlerDifferential.D R (MvPolynomial σ R)) (MvPolynomial.X i)) =
    fun₀ | i => 1
-- Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
/-- Constructor for elements in a pullback in a concrete category.  -/
CategoryTheory.Limits.Concrete.pullbackMk : {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)] →
                      (x₁ : CategoryTheory.ToType X₁) →
                        (x₂ : CategoryTheory.ToType X₂) →
                          (CategoryTheory.ConcreteCategory.hom f₁) x₁ = (CategoryTheory.ConcreteCategory.hom f₂) x₂ →
                            CategoryTheory.ToType (CategoryTheory.Limits.pullback f₁ f₂)
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instNonUnitalRingOfIsTopologicalRing : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : NonUnitalRing β] → [IsTopologicalRing β] → NonUnitalRing (CompactlySupportedContinuousMap α β)
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instAddLeftCancelSemigroup.eq_1 : ∀ {α : Type u_1} [inst : AddLeftCancelSemigroup α],
  Lex.instAddLeftCancelSemigroup = { toAddSemigroup := Lex.instAddSemigroup, toIsLeftCancelAdd := ⋯ }
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup
FundamentalGroup.inv_def : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X} {p : FundamentalGroup X x}, p⁻¹ = Path.Homotopic.Quotient.symm p
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get_union_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α} (mem : k ∈ m₂), (m₁ ∪ m₂).get k ⋯ = m₂.get k mem
-- Init.Data.BitVec.Basic
/-- Signed less-than for bitvectors.

SMT-LIB name: `bvslt`.

Examples:
* `BitVec.slt 6#4 7 = true`
* `BitVec.slt 7#4 8 = false`
 -/
BitVec.slt : {n : ℕ} → BitVec n → BitVec n → Bool
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- Lagrange's **Mean Value Theorem**, `deriv` version.  -/
exists_deriv_eq_slope : ∀ (f : ℝ → ℝ) {a b : ℝ},
  a < b →
    ContinuousOn f (Set.Icc a b) →
      DifferentiableOn ℝ f (Set.Ioo a b) → ∃ c ∈ Set.Ioo a b, deriv f c = (f b - f a) / (b - a)
-- Batteries.Data.MLList.Basic
/-- Convert an array to a monadic lazy list.  -/
MLList.ofArray : {m : Type → Type} → {α : Type} → Array α → MLList m α
-- Mathlib.Data.Matrix.Composition
Matrix.compRingEquiv_apply : ∀ (I : Type u_1) (J : Type u_2) (R : Type u_5) [inst : AddCommMonoid R] [inst_1 : Mul R] [inst_2 : Fintype I]
  [inst_3 : Fintype J] (M : Matrix I I (Matrix J J R)), (Matrix.compRingEquiv I J R) M = (Matrix.comp I I J J R) M
-- Mathlib.Order.Interval.Finset.Basic
Finset.Icc_subset_Ico_right : ∀ {α : Type u_2} {a b₁ b₂ : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α],
  b₁ < b₂ → Finset.Icc a b₁ ⊆ Finset.Ico a b₂
-- Lean.Elab.PreDefinition.Basic
Lean.Elab.ensureNoRecFn : Array Lean.Name → Lean.Expr → Lean.MetaM Unit
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.support_mapLe_eq_support : ∀ {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} (p : G.Walk u v),
  (SimpleGraph.Walk.mapLe h p).support = p.support
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.iterate_frobenius_mk : ∀ (K : Type u) [inst : CommRing K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p] (n : ℕ) (x : K),
  (⇑(frobenius (PerfectClosure K p) p))^[n] (PerfectClosure.mk K p (n, x)) = (PerfectClosure.of K p) x
-- Mathlib.Order.Copy
/-- A function to create a provable equal copy of a heyting algebra
with possibly different definitional equalities.  -/
HeytingAlgebra.copy : {α : Type u} →
  (c : HeytingAlgebra α) →
    (le : α → α → Prop) →
      le = LE.le →
        (top : α) →
          top = ⊤ →
            (bot : α) →
              bot = ⊥ →
                (sup : α → α → α) →
                  sup = max →
                    (inf : α → α → α) →
                      inf = min →
                        (himp : α → α → α) → himp = HImp.himp → (compl : α → α) → compl = Compl.compl → HeytingAlgebra α
-- Mathlib.Data.Set.Card
Set.even_card_insert_iff : ∀ {α : Type u_1} {s : Set α} {a : α},
  a ∉ s → autoParam s.Finite Set.even_card_insert_iff._auto_1 → (Even (insert a s).ncard ↔ Odd s.ncard)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.congrIndexOneOfEq.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {i i' j j' : E.I₀} (hii' : i = i') (hjj' : j = j'),
  CategoryTheory.PreOneHypercover.congrIndexOneOfEq hii' hjj' =
    CategoryTheory.PreOneHypercover.congrIndexOneOfEq hii' hjj'
-- Mathlib.LinearAlgebra.Matrix.Swap
/-- Multiplying with `swap R i j` on the right swaps the `i`-th column with the `j`-th column.  -/
Matrix.mul_swap_apply_left : ∀ {R : Type u_1} {n : Type u_2} {m : Type u_3} [inst : Semiring R] [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  (i j : n) (a : m) (g : Matrix m n R), (g * Matrix.swap R i j) a i = g a j
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.skeletonOfMono.eq_1 : ∀ {X Y : SSet} (i : X ⟶ Y),
  SSet.skeletonOfMono i = { toFun := fun n => SSet.Subcomplex.range i ⊔ Y.skeleton n, monotone' := ⋯ }
-- Mathlib.Logic.Basic
/-- **Alias** of `Classical.imp_iff_right_iff`. -/
imp_iff_right_iff : ∀ {a b : Prop}, (a → b ↔ b) ↔ a ∨ b
-- Mathlib.Order.Interval.Set.Basic
/-- In an order without maximal elements, the intervals `Ioi` are nonempty.  -/
Set.nonempty_Ioi_subtype : ∀ {α : Type u_1} [inst : Preorder α] {a : α} [NoMaxOrder α], Nonempty ↑(Set.Ioi a)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- A function is differentiable on two open sets iff it is differentiable on their union.  -/
mdifferentiableOn_union_iff_of_isOpen : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s t : Set M},
  IsOpen s → IsOpen t → (MDiff[s ∪ t] f ↔ MDiff[s] f ∧ MDiff[t] f)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
lt_inv_iff_mul_lt_one' : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulLeftStrictMono α] {a b : α}, a < b⁻¹ ↔ b * a < 1
-- Lean.Parser.Basic
Lean.Parser.TokenMap.instForInProdNameListOfMonad : {m : Type u_1 → Type u_2} → {α : Type} → [Monad m] → ForIn m (Lean.Parser.TokenMap α) (Lean.Name × List α)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.smul_mk : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {R : Type u_4} [inst_1 : SMul R M]
  [inst_2 : IsScalarTower R M M] (c : R) (a : M) (b : ↥S), c • Localization.mk a b = Localization.mk (c • a) b
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ChangeAnnotationSupport.mk.sizeOf_spec : ∀ (groupsOnLabel? : Option Bool), sizeOf { groupsOnLabel? := groupsOnLabel? } = 1 + sizeOf groupsOnLabel?
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.endsWith_bool_iff_get : ∀ {p : Char → Bool} {s : String},
  s.endsWith p = true ↔ ∃ (h : s.endPos ≠ s.startPos), p ((s.endPos.prev h).get ⋯) = true
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.resultant_integralNormalization : ∀ {R : Type u_1} [inst : CommRing R] (f g : Polynomial R),
  g.natDegree ≠ 0 →
    (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization =
      g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.zmodEquivZPowers_symm_apply_pow' : ∀ {R : Type u_4} {k : ℕ} [inst : CommRing R] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) (i : ℕ),
  h.zmodEquivZPowers.symm ⟨ζ ^ i, ⋯⟩ = ↑i
-- Mathlib.Data.Char
/-- Provides a `LinearOrder` instance on `Char`. `Char` is the type of Unicode scalar values.
 -/
instLinearOrderChar : LinearOrder Char
-- Mathlib.Data.EReal.Basic
instOneEReal : One EReal
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupNorm.lt_def : ∀ {E : Type u_3} [inst : AddGroup E] {p q : NonarchAddGroupNorm E}, p < q ↔ ⇑p < ⇑q
-- Init.Data.Int.DivMod.Lemmas
Int.sub_mul_ediv_left : ∀ (a : ℤ) {b : ℤ} (c : ℤ), b ≠ 0 → (a - b * c) / b = a / b - c
-- Mathlib.SetTheory.Ordinal.Notation
/-- Comparison of ordinal notations:

`ω ^ e₁ * n₁ + a₁` is less than `ω ^ e₂ * n₂ + a₂` when either `e₁ < e₂`, or `e₁ = e₂` and
`n₁ < n₂`, or `e₁ = e₂`, `n₁ = n₂`, and `a₁ < a₂`.  -/
ONote.cmp : ONote → ONote → Ordering
-- Mathlib.Analysis.Meromorphic.Order
/-- The order of `(· - x) ^ n` at `x` is `n`.  -/
meromorphicOrderAt_zpow_id_sub_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {n : ℤ},
  meromorphicOrderAt ((fun x_1 => x_1 - x) ^ n) x = ↑n
-- Mathlib.Order.RelIso.Basic
/-- A relation embedding with respect to a given pair of relations `r` and `s`
is an embedding `f : α ↪ β` such that `r a b ↔ s (f a) (f b)`.  -/
«term_↪r_» : Lean.TrailingParserDescr
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.State.mk.sizeOf_spec : ∀ (argPos targetPos : ℕ) (motive : Option Lean.MVarId) (f fType : Lean.Expr) (alts : Array Lean.Elab.Tactic.ElimApp.Alt)
  (insts : Array Lean.MVarId),
  sizeOf
      { argPos := argPos, targetPos := targetPos, motive := motive, f := f, fType := fType, alts := alts,
        insts := insts } =
    1 + sizeOf argPos + sizeOf targetPos + sizeOf motive + sizeOf f + sizeOf fType + sizeOf alts + sizeOf insts
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
/-- The morphism `X.toNormalizedChainComplex R` for any simplicial set `X`,
as a natural transformation.  -/
SSet.toNormalizedChainComplexNatTrans : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasCoproducts C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        (R : C) → (SSet.chainComplexFunctor C).obj R ⟶ SSet.normalizedChainComplexFunctorObj R
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.lift₃.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Full] {A₁ A₂ A₃ : C} {X : D} {f₁ : F.obj A₁ ⟶ X}
  (hf₁ : F.relativelyRepresentable f₁) (f₂ : F.obj A₂ ⟶ X) (f₃ : F.obj A₃ ⟶ X)
  [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)] [inst_4 : F.Faithful] {Z : C} (x₁ : Z ⟶ A₁)
  (x₂ : Z ⟶ A₂) (x₃ : Z ⟶ A₃)
  (h₁₂ : CategoryTheory.CategoryStruct.comp (F.map x₁) f₁ = CategoryTheory.CategoryStruct.comp (F.map x₂) f₂)
  (h₁₃ : CategoryTheory.CategoryStruct.comp (F.map x₁) f₁ = CategoryTheory.CategoryStruct.comp (F.map x₃) f₃),
  hf₁.lift₃ f₂ f₃ x₁ x₂ x₃ h₁₂ h₁₃ = CategoryTheory.Limits.pullback.lift (hf₁.lift' x₁ x₂ h₁₂) (hf₁.lift' x₁ x₃ h₁₃) ⋯
-- Mathlib.Data.Finset.Insert
/-- To prove a proposition about an arbitrary `Finset α`,
it suffices to prove it for the empty `Finset`,
and to show that if it holds for some `Finset α`,
then it holds for the `Finset` obtained by inserting a new element.
 -/
Finset.induction_on : ∀ {α : Type u_3} {motive : Finset α → Prop} [inst : DecidableEq α] (s : Finset α),
  motive ∅ → (∀ (a : α) (s : Finset α), a ∉ s → motive s → motive (insert a s)) → motive s
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.instInhabited : Inhabited Cardinal.{u}
-- Mathlib.Data.Set.Subset
Set.image_val_inj : ∀ {α : Type u_2} {A : Set α} {D E : Set ↑A}, Subtype.val '' D = Subtype.val '' E ↔ D = E
-- Init.Data.Vector.Lex
Vector.not_le_iff_gt : ∀ {α : Type u_1} {n : ℕ} [inst : LT α] {xs ys : Vector α n}, ¬xs ≤ ys ↔ ys < xs
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.of_symm_zero : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Zero α], Matrix.of.symm 0 = 0
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.symmetry : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X Y : CategoryTheory.Dial C),
  CategoryTheory.CategoryStruct.comp (X.braiding Y).hom (Y.braiding X).hom =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.RingedSpace.basicOpen.eq_1 : ∀ (X : AlgebraicGeometry.RingedSpace) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace}
  (f : ↑(X.presheaf.obj (Opposite.op U))),
  X.basicOpen f =
    { carrier := {x | ∃ (hx : x ∈ U), IsUnit ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x hx)) f)},
      is_open' := ⋯ }
-- Mathlib.Analysis.Complex.Harmonic.Analytic
InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_ball_re_eq : ∀ {f : ℂ → ℝ} {z : ℂ} {R : ℝ},
  InnerProductSpace.HarmonicOnNhd f (Metric.ball z R) →
    ∃ F, AnalyticOnNhd ℂ F (Metric.ball z R) ∧ Set.EqOn (fun z => (F z).re) f (Metric.ball z R)
-- Mathlib.Algebra.Category.ModuleCat.EnoughInjectives
instEnoughInjectivesModuleCatOfSmall : ∀ (R : Type u) [inst : Ring R] [Small.{v, u} R], CategoryTheory.EnoughInjectives (ModuleCat R)
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.norm_add_eq_max_of_ne : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {q r : ℤ_[p]}, ‖q‖ ≠ ‖r‖ → ‖q + r‖ = max ‖q‖ ‖r‖
-- Mathlib.Analysis.Normed.Ring.Basic
NormMulClass.isAbsoluteValue_norm : ∀ {α : Type u_2} [inst : NormedRing α] [NormMulClass α], IsAbsoluteValue norm
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.isCyclic_iff : ∀ {n : ℕ}, IsCyclic (DihedralGroup n) ↔ n = 1
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabMProdMk : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
/-- The pushout cocone attached to a commutative square.  -/
CategoryTheory.Square.pushoutCocone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (sq : CategoryTheory.Square C) → CategoryTheory.Limits.PushoutCocone sq.f₁₂ sq.f₁₃
-- Mathlib.CategoryTheory.Filtered.Small
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsCofiltered.CofilteredClosureSmall.InductiveStep.eq : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {n : ℕ} →
      {X : (k : ℕ) → k < n → (t : Type (max v w)) × (t → C)} →
        {k k' : ℕ} →
          (hk : k < n) →
            (hk' : k' < n) →
              (j : (X k hk).fst) →
                (j' : (X k' hk').fst) →
                  ((X k hk).snd j ⟶ (X k' hk').snd j') →
                    ((X k hk).snd j ⟶ (X k' hk').snd j') →
                      CategoryTheory.IsCofiltered.CofilteredClosureSmall.InductiveStep✝ n X
-- Lean.Data.Lsp.Extra
Lean.Lsp.instInhabitedDependencyBuildMode.default : Lean.Lsp.DependencyBuildMode
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.mk.injEq : ∀ {J : CategoryTheory.Limits.MulticospanShape} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (left : J.L → C)
  (right : J.R → C) (fst : (b : J.R) → left (J.fst b) ⟶ right b) (snd : (b : J.R) → left (J.snd b) ⟶ right b)
  (left_1 : J.L → C) (right_1 : J.R → C) (fst_1 : (b : J.R) → left_1 (J.fst b) ⟶ right_1 b)
  (snd_1 : (b : J.R) → left_1 (J.snd b) ⟶ right_1 b),
  ({ left := left, right := right, fst := fst, snd := snd } =
      { left := left_1, right := right_1, fst := fst_1, snd := snd_1 }) =
    (left = left_1 ∧ right = right_1 ∧ fst ≍ fst_1 ∧ snd ≍ snd_1)
-- Mathlib.Algebra.Module.Equiv.Basic
/-- Given an `R`-module `M` and an equivalence `m ≃ n` between arbitrary types,
construct a linear equivalence `(n → M) ≃ₗ[R] (m → M)`  -/
LinearEquiv.funCongrLeft : (R : Type u_1) →
  (M : Type u_5) →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → {m : Type u_9} → {n : Type u_10} → m ≃ n → (n → M) ≃ₗ[R] m → M
-- Init.Data.SInt.Basic
instComplementInt8 : Complement Int8
-- Init.Data.UInt.Lemmas
UInt16.sub_self : ∀ (a : UInt16), a - a = 0
-- Mathlib.Control.Traversable.Instances
List.traverse.eq_1 : ∀ {F : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Applicative F] (f : α → F β),
  List.traverse f [] = pure []
-- Init.Data.String.Basic
String.data_inj : ∀ {s₁ s₂ : String}, s₁.toList = s₂.toList ↔ s₁ = s₂
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_sub_const_Ico : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b c : α),
  (fun x => x - a) '' Set.Ico b c = Set.Ico (b - a) (c - a)
-- Lean.ProjFns
/-- `true` if the structure is a class.  -/
Lean.ProjectionFunctionInfo.fromClass : Lean.ProjectionFunctionInfo → Bool
-- Mathlib.Topology.Order.Hom.Esakia
EsakiaHomClass.toPseudoEpimorphismClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : TopologicalSpace α]
  [inst_2 : Preorder α] [inst_3 : TopologicalSpace β] [inst_4 : Preorder β] [EsakiaHomClass F α β],
  PseudoEpimorphismClass F α β
-- Mathlib.Data.Fin.Tuple.Reflection
_private.Mathlib.Data.Fin.Tuple.Reflection.0.FinVec.Forall.match_1.eq_2 : ∀ {α : Type u_2} (motive : (x : ℕ) → ((Fin x → α) → Prop) → Sort u_1) (n : ℕ) (P : (Fin (n + 1) → α) → Prop)
  (h_1 : (P : (Fin 0 → α) → Prop) → motive 0 P) (h_2 : (n : ℕ) → (P : (Fin (n + 1) → α) → Prop) → motive n.succ P),
  (match n.succ, P with
    | 0, P => h_1 P
    | n.succ, P => h_2 n P) =
    h_2 n P
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_inf : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {s : Finset β} {f g : β → α},
  s.inf (f ⊓ g) = s.inf f ⊓ s.inf g
-- Mathlib.Algebra.ContinuedFractions.TerminatedStable
GenContFract.nums_stable_of_terminated : ∀ {K : Type u_1} {g : GenContFract K} {n m : ℕ} [inst : DivisionRing K], n ≤ m → g.TerminatedAt n → g.nums m = g.nums n
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.point_logSizeBallSeq_add_one : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [inst_1 : DecidableEq T] (hJ : J.Nonempty)
  (i : ℕ),
  (PairReduction.logSizeBallSeq J hJ a c (i + 1)).point =
    if hV' : (PairReduction.logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty then Exists.choose hV'
    else (PairReduction.logSizeBallSeq J hJ a c i).point
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey?_le_minKey?_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {k km kme : α} (hkme : (t.erase k).minKey? = some kme), t.minKey?.get ⋯ = km → (cmp km kme).isLE = true
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.pow_le_of_le_log : ∀ {x y : ℝ} {n : ℕ}, 0 < y → Real.log x ≤ ↑n * Real.log y → x ≤ y ^ n