mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Sheaves.LocalPredicate
TopCat.stalkToFiber_ι : ∀ {X : TopCat} {T : ↑X → Type u_1} (P : TopCat.LocalPredicate T) (x : ↑X) (U : (TopologicalSpace.OpenNhds x)ᵒᵖ)
  (fU : { f // P.pred f }),
  (CategoryTheory.ConcreteCategory.hom (TopCat.stalkToFiber P x))
      ((CategoryTheory.ConcreteCategory.hom
          (CategoryTheory.Limits.colimit.ι
            ((TopologicalSpace.OpenNhds.inclusion x).op.comp (TopCat.subpresheafToTypes P.toPrelocalPredicate)) U))
        fU) =
    (CategoryTheory.ConcreteCategory.hom ((P.cocone x).ι.app U)) fU
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.ι_range_comap_involute : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M),
  Submodule.comap CliffordAlgebra.involute.toLinearMap (CliffordAlgebra.ι Q).range = (CliffordAlgebra.ι Q).range
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_eq_map : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {W : CategoryTheory.MorphismProperty C}
  [inst_2 : W.HasLeftCalculusOfFractions] {X Y Z : C} (z₁ : W.LeftFraction X Y) (z₂ : W.LeftFraction Y Z)
  (z₃ : W.LeftFraction z₁.Y' z₂.Y'),
  CategoryTheory.CategoryStruct.comp z₂.f z₃.s = CategoryTheory.CategoryStruct.comp z₁.s z₃.f →
    ∀ (L : CategoryTheory.Functor C D) [inst_3 : L.IsLocalization W],
      CategoryTheory.CategoryStruct.comp (z₁.map L ⋯) (z₂.map L ⋯) = (z₁.comp₀ z₂ z₃).map L ⋯
-- Mathlib.FieldTheory.JacobsonNoether
/-- Jacobson-Noether theorem: For a non-commutative division algebra
`D` that is algebraic over its center `k`, there exists an element
`x` of `D \ k` that is separable over `k`.  -/
JacobsonNoether.exists_separable_and_not_isCentral : ∀ (D : Type u_1) [inst : DivisionRing D] [Algebra.IsAlgebraic (↥(Subring.center D)) D],
  Subring.center D ≠ ⊤ → ∃ x ∉ Subring.center D, IsSeparable (↥(Subring.center D)) x
-- Mathlib.Algebra.GroupWithZero.ProdHom
MonoidWithZeroHom.inl_injective : ∀ {G₀ : Type u_1} {H₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : GroupWithZero H₀]
  [inst_2 : DecidablePred fun x => x = 0], Function.Injective ⇑(MonoidWithZeroHom.inl G₀ H₀)
-- Init.Data.String.Iterate
String.Slice.instInhabitedPosIterator.default : {s : String.Slice} → s.PosIterator
-- Mathlib.Analysis.InnerProductSpace.Calculus
deriv_inner_apply : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : NormedSpace ℝ E] {f g : ℝ → E} {x : ℝ},
  DifferentiableAt ℝ f x →
    DifferentiableAt ℝ g x →
      deriv (fun t => inner 𝕜 (f t) (g t)) x = inner 𝕜 (f x) (deriv g x) + inner 𝕜 (deriv f x) (g x)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.IsRamified.liesOver_isReal_under : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (w : NumberField.InfinitePlace L) (v : NumberField.InfinitePlace K) [w.LiesOver v],
  NumberField.InfinitePlace.IsRamified K w → v.IsReal
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- In a nonempty graph, the minimal degree is less than the number of vertices.  -/
SimpleGraph.minDegree_lt_card : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj] [Nonempty V],
  G.minDegree < Fintype.card V
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.instDecidableEqList.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (head : α) (tail : List α) (h_1 : Unit → motive [])
  (h_2 : (head : α) → (tail : List α) → motive (head :: tail)),
  (match head :: tail with
    | [] => h_1 ()
    | head :: tail => h_2 head tail) =
    h_2 head tail
-- Std.Sat.AIG.LawfulOperator
/-- If `decls1` is a prefix of `decls2` and we start evaluating `decls2` at an
index in bounds of `decls1` we can evaluate at `decls1`.
 -/
Std.Sat.AIG.denote.eq_of_isPrefix : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {assign : α → Bool} (entry : Std.Sat.AIG.Entrypoint α)
  (newAIG : Std.Sat.AIG α) (hprefix : Std.Sat.AIG.IsPrefix entry.aig.decls newAIG.decls),
  ⟦assign, { aig := newAIG, ref := { gate := entry.ref.gate, invert := entry.ref.invert, hgate := ⋯ } }⟧ =
    ⟦assign, entry⟧
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!_union_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} [inst_1 : Inhabited (β k)], k ∉ t₂ → (t₁ ∪ t₂).get! k = t₁.get! k
-- Init.Omega.IntList
Lean.Omega.IntList.instNeg : Neg Lean.Omega.IntList
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
_private.Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic.0.Std.Tactic.BVDecide.Gate.toString.match_1.eq_2 : ∀ (motive : Std.Tactic.BVDecide.Gate → Sort u_1) (h_1 : Unit → motive Std.Tactic.BVDecide.Gate.and)
  (h_2 : Unit → motive Std.Tactic.BVDecide.Gate.xor) (h_3 : Unit → motive Std.Tactic.BVDecide.Gate.beq)
  (h_4 : Unit → motive Std.Tactic.BVDecide.Gate.or),
  (match Std.Tactic.BVDecide.Gate.xor with
    | Std.Tactic.BVDecide.Gate.and => h_1 ()
    | Std.Tactic.BVDecide.Gate.xor => h_2 ()
    | Std.Tactic.BVDecide.Gate.beq => h_3 ()
    | Std.Tactic.BVDecide.Gate.or => h_4 ()) =
    h_2 ()
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.maxKey_modifyKey_beq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : β → β} {he : (Std.Internal.List.Const.modifyKey k f l).isEmpty = false},
      (Std.Internal.List.maxKey (Std.Internal.List.Const.modifyKey k f l) he == Std.Internal.List.maxKey l ⋯) = true
-- Init.Grind.Ordered.Field
_private.Init.Grind.Ordered.Field.0.Lean.Grind.Field.IsOrdered.lt_mul_of_lt_mul_inv : ∀ {R : Type u} [inst : Lean.Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] {a b c : R}, c < 0 → a < b * c⁻¹ → b < a * c
-- Init.Conv
Lean.Parser.Tactic.Conv.convSeq1Indented : Lean.ParserDescr
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.mk_intCast : ∀ {S : Type u_3} [inst : LinearOrder S] [inst_1 : CommRing S] [inst_2 : IsStrictOrderedRing S] {n : ℤ},
  n ≠ 0 → ArchimedeanClass.mk ↑n = 0
-- Mathlib.Order.Nucleus
/-- A nucleus is an inflationary idempotent `inf`-preserving endomorphism of a semilattice.

In a frame, nuclei correspond to sublocales. See `nucleusIsoSublocale`.  -/
Nucleus : (X : Type u_2) → [SemilatticeInf X] → Type u_2
-- Batteries.Lean.EStateM
_private.Batteries.Lean.EStateM.0.EStateM.run_orElse.match_1.eq_1 : ∀ {σ ε α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (x : α) (s : σ)
  (h_1 : (x : α) → (s : σ) → motive (EStateM.Result.ok x s))
  (h_2 : (a : ε) → (s' : σ) → motive (EStateM.Result.error a s')),
  (match EStateM.Result.ok x s with
    | EStateM.Result.ok x s => h_1 x s
    | EStateM.Result.error a s' => h_2 a s') =
    h_1 x s
-- Mathlib.Data.List.Shortlex
List.shortlex_singleton_iff : ∀ {α : Type u_1} {r : α → α → Prop} (a b : α), List.Shortlex r [a] [b] ↔ r a b
-- Mathlib.CategoryTheory.SingleObj
CategoryTheory.SingleObj.mapHom_id : ∀ (M : Type u) [inst : Monoid M],
  (CategoryTheory.SingleObj.mapHom M M) (MonoidHom.id M) = CategoryTheory.Functor.id (CategoryTheory.SingleObj M)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_ofNat : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : MulOneClass M] (n : ℕ) [inst_2 : n.AtLeastTwo],
  (OfNat.ofNat n).coeff = fun₀ | 1 => OfNat.ofNat n
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.div_inter_subset : ∀ {α : Type u_2} [inst : Div α] {s t₁ t₂ : Set α}, s / (t₁ ∩ t₂) ⊆ s / t₁ ∩ (s / t₂)
-- Init.Data.SInt.Lemmas
Int32.toBitVec_ofNat' : ∀ {n : ℕ}, (Int32.ofNat n).toBitVec = BitVec.ofNat 32 n
-- Mathlib.Algebra.BigOperators.Finprod
/-- See also `finsum_eq_of_bijective`, `Fintype.sum_bijective` and `Finset.sum_bij`.  -/
finsum_comp : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {g : β → M} (e : α → β),
  Function.Bijective e → ∑ᶠ (i : α), g (e i) = ∑ᶠ (j : β), g j
-- Mathlib.GroupTheory.Index
AddSubgroup.index_top : ∀ {G : Type u_1} [inst : AddGroup G], ⊤.index = 1
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.eq_succMany?_of_toArray_eq_append_append : ∀ {α : Type u} {r : Std.Ric α} [inst : Std.PRange.Least? α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerableLE α] [inst_6 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxc.IsAlwaysFinite α] {pref suff : Array α} {cur : α} (h : r.toArray = pref ++ #[cur] ++ suff),
  cur = (Std.PRange.succMany? pref.size Std.PRange.UpwardEnumerable.least).get ⋯
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
range_cfcₙ_eq_range_cfcₙHom : ∀ (R : Type u_1) {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] {a : A} (ha : p a),
  (Set.range fun x => cfcₙ x a) = ↑(NonUnitalStarAlgHom.range (cfcₙHom ha))
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda_inv_comp_π : ∀ {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] (i : I),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda F).inv
      (CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F i).op) =
    CategoryTheory.Limits.limit.π (F.op.comp CategoryTheory.coyoneda) (Opposite.op i)
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.vaddConst_toAffineEquiv : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] (p : P),
  (AffineIsometryEquiv.vaddConst 𝕜 p).toAffineEquiv = AffineEquiv.vaddConst 𝕜 p
-- Lean.Parser.Term
/-- `-opt` is short for `(opt := false)`. It sets the `opt` configuration option to `false`.
 -/
Lean.Parser.Term.negConfigItem : Lean.Parser.Parser
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.trivialCofibrations_op : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithFibrations C],
  HomotopicalAlgebra.trivialCofibrations Cᵒᵖ = (HomotopicalAlgebra.trivialFibrations C).op
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.homEquivOfIsRightKanExtension.congr_simp : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α α_1 : L.comp F' ⟶ F) (e_α : α = α_1) [inst_3 : F'.IsRightKanExtension α] (G : CategoryTheory.Functor D H),
  F'.homEquivOfIsRightKanExtension α G = F'.homEquivOfIsRightKanExtension α_1 G
-- Aesop.Tree.UnsafeQueue
Aesop.UnsafeQueueEntry.unsafeRule.sizeOf_spec : ∀ (r : Aesop.IndexMatchResult Aesop.UnsafeRule), sizeOf (Aesop.UnsafeQueueEntry.unsafeRule r) = 1 + sizeOf r
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
DifferentiableAt.log : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E},
  DifferentiableAt ℝ f x → f x ≠ 0 → DifferentiableAt ℝ (fun x => Real.log (f x)) x
-- Mathlib.LinearAlgebra.Matrix.Integer
Matrix.num_transpose : ∀ {m : Type u_1} {n : Type u_2} [inst : Fintype m] [inst_1 : Fintype n] (A : Matrix m n ℚ),
  A.transpose.num = A.num.transpose
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.toCols₁_fromCols : ∀ {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R),
  (A₁.fromCols A₂).toCols₁ = A₁
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.instSupSet.eq_1 : ∀ {α : Type u_1} [inst : LE α], UpperSet.instSupSet = { sSup := fun S => { carrier := ⋂ s ∈ S, ↑s, upper' := ⋯ } }
-- Mathlib.NumberTheory.Divisors
Nat.mem_properDivisors : ∀ {n m : ℕ}, n ∈ m.properDivisors ↔ n ∣ m ∧ n < m
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The forward map of a homeomorphism is a continuous function.  -/
ContinuousMulEquiv.continuous_toFun : ∀ {G : Type u} [inst : TopologicalSpace G] {H : Type v} [inst_1 : TopologicalSpace H] [inst_2 : Mul G] [inst_3 : Mul H]
  (self : G ≃ₜ* H), Continuous self.toFun
-- Mathlib.Order.Monotone.Defs
MonotoneOn.comp_AntitoneOn : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
  {f : α → β} {s : Set α} {t : Set β}, MonotoneOn g t → AntitoneOn f s → Set.MapsTo f s t → AntitoneOn (g ∘ f) s
-- Mathlib.CategoryTheory.Yoneda
/-- Unification hint for `(coyoneda.obj Y).obj X = unop Y ⟶ X`.  -/
CategoryTheory.coyoneda_obj_obj_eq_hom' : {C : Type u₁} → [CategoryTheory.Category.{v₁, u₁} C] → C → C → Cᵒᵖ → Cᵒᵖ → Prop
-- Mathlib.Topology.Order.OrderClosed
IsLUB.range_of_tendsto : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [ClosedIicTopology α] {f : β → α} {a : α}
  {F : Filter β} [F.NeBot], (∀ (i : β), f i ≤ a) → Filter.Tendsto f F (nhds a) → IsLUB (Set.range f) a
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
mul_mem_nonZeroDivisorsRight_of_mem_nonZeroDivisorsRight : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {x y : M₀},
  x ∈ nonZeroDivisorsRight M₀ → y ∈ nonZeroDivisorsRight M₀ → x * y ∈ nonZeroDivisorsRight M₀
-- Mathlib.Topology.Order.LeftRight
nhdsLE_neBot : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α] (a : α), (nhdsWithin a (Set.Iic a)).NeBot
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddEquiv.subsemigroupMap_symm_apply_coe : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (e : M ≃+ N) (S : AddSubsemigroup M)
  (x : ↥(AddSubsemigroup.map (↑e) S)), ↑((e.subsemigroupMap S).symm x) = e.symm ↑x
-- Mathlib.CategoryTheory.Sums.Associator
/-- The equivalence of categories expressing associativity of sums of categories.
 -/
CategoryTheory.sum.associativity : (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] → (C ⊕ D) ⊕ E ≌ C ⊕ D ⊕ E
-- Mathlib.Topology.Algebra.ConstMulAction
IsUnit.continuousWithinAt_const_smul_iff : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Monoid M] [inst_1 : TopologicalSpace α] [inst_2 : MulAction M α]
  [ContinuousConstSMul M α] [inst_4 : TopologicalSpace β] {f : β → α} {b : β} {c : M} {s : Set β},
  IsUnit c → (ContinuousWithinAt (fun x => c • f x) s b ↔ ContinuousWithinAt f s b)
-- Mathlib.RingTheory.AlgebraicIndependent.Transcendental
AlgebraicIndependent.transcendental_adjoin : ∀ {ι : Type u_1} {R : Type u_3} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A],
  AlgebraicIndependent R x → ∀ {s : Set ι} {i : ι}, i ∉ s → Transcendental (↥(Algebra.adjoin R (x '' s))) (x i)
-- Mathlib.Analysis.Convex.Mul
ConcaveOn.smul_convexOn' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : CommRing 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : CommRing E] [inst_4 : LinearOrder E] [IsStrictOrderedRing E]
  [inst_6 : AddCommGroup F] [inst_7 : LinearOrder F] [IsOrderedAddMonoid F] [inst_9 : AddCommGroup G]
  [inst_10 : Module 𝕜 G] [inst_11 : Module 𝕜 E] [inst_12 : Module 𝕜 F] [inst_13 : Module E F] [IsScalarTower 𝕜 E F]
  [SMulCommClass 𝕜 E F] [IsOrderedModule 𝕜 F] [IsStrictOrderedModule E F] {s : Set G} {f : G → E} {g : G → F},
  ConcaveOn 𝕜 s f →
    ConvexOn 𝕜 s g →
      (∀ ⦃x : G⦄, x ∈ s → f x ≤ 0) → (∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x) → AntivaryOn f g s → ConcaveOn 𝕜 s (f • g)
-- Mathlib.Data.Matrix.Diagonal
Matrix.diagonal_eq_intCast : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : IntCast α] {d : n → α} {m : ℤ},
  Matrix.diagonal d = ↑m ↔ d = ↑m
-- Mathlib.Order.Concept
Concept.rel_extent_intent : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c : Concept α β r} {x : α} {y : β},
  x ∈ c.extent → y ∈ c.intent → r x y
-- Mathlib.GroupTheory.SchurZassenhaus
/-- Do not use this lemma: It is made obsolete by `exists_right_complement'_of_coprime`  -/
_private.Mathlib.GroupTheory.SchurZassenhaus.0.Subgroup.SchurZassenhausInduction.step5 : ∀ {G : Type u} [inst : Group G] {N : Subgroup G} [N.Normal],
  (Nat.card ↥N).Coprime N.index →
    (∀ (H : Subgroup G), ¬N.IsComplement' H) → ∀ [Finite G] {P : Sylow (Nat.card ↥N).minFac ↥N}, ↑P ≠ ⊥
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The induced functor to `Under X` from a functor `J ⥤ C` and natural maps `sᵢ : X ⟶ Dᵢ`.  -/
CategoryTheory.Under.lift : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {J : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} J] →
        (D : CategoryTheory.Functor J T) →
          {X : T} → ((CategoryTheory.Functor.const J).obj X ⟶ D) → CategoryTheory.Functor J (CategoryTheory.Under X)
-- Mathlib.Topology.UniformSpace.Defs
subset_comp_self_of_mem_uniformity : ∀ {α : Type ua} [inst : UniformSpace α] {s : SetRel α α}, s ∈ uniformity α → s ⊆ s.comp s
-- Mathlib.Algebra.Homology.ShortComplex.Limits
/-- If a cocone with values in `ShortComplex C` is such that it becomes colimit
when we apply the three projections `ShortComplex C ⥤ C`, then it is colimit.  -/
CategoryTheory.ShortComplex.isColimitOfIsColimitπ : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          {F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)} →
            (c : CategoryTheory.Limits.Cocone F) →
              CategoryTheory.Limits.IsColimit (CategoryTheory.ShortComplex.π₁.mapCocone c) →
                CategoryTheory.Limits.IsColimit (CategoryTheory.ShortComplex.π₂.mapCocone c) →
                  CategoryTheory.Limits.IsColimit (CategoryTheory.ShortComplex.π₃.mapCocone c) →
                    CategoryTheory.Limits.IsColimit c
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- The trivial group object.  -/
CategoryTheory.Grp.trivial : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → CategoryTheory.Grp C
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
HasSum.compl_add : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a b : α}
  [ContinuousAdd α] {s : Set β}, HasSum (f ∘ Subtype.val) a → HasSum (f ∘ Subtype.val) b → HasSum f (a + b)
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.FlatMap.0.Std.Iter.step_flatMapAfter.match_1.eq_1 : ∀ {α₂ γ : Type u_1} (motive : Option (Std.Iter γ) → Sort u_2) (h_1 : Unit → motive none)
  (h_2 : (it₂ : Std.Iter γ) → motive (some it₂)),
  (match none with
    | none => h_1 ()
    | some it₂ => h_2 it₂) =
    h_1 ()
-- Mathlib.Data.Vector.MapLemmas
/-- If there is a set of states that is closed under `f`, and such that `f` produces that same output
for all states in this set, then the state is not actually needed.
Hence, then we can rewrite `mapAccumr` into just `map`.
 -/
List.Vector.mapAccumr_eq_map : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_5} {n : ℕ} {xs : List.Vector α n} {f : α → σ → σ × β} {s₀ : σ} (S : Set σ),
  s₀ ∈ S →
    (∀ (a : α), ∀ s ∈ S, (f a s).1 ∈ S) →
      (∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).2 = (f a s').2) →
        (List.Vector.mapAccumr f xs s₀).2 = List.Vector.map (fun x => (f x s₀).2) xs
-- Mathlib.Algebra.Category.Ring.Basic
SemiRingCat.forgetReflectIsos : (CategoryTheory.forget SemiRingCat).ReflectsIsomorphisms
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.cauchy₂ : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [IsAbsoluteValue abv] (f : CauSeq β abv) {ε : α},
  0 < ε → ∃ i, ∀ j ≥ i, ∀ k ≥ i, abv (↑f j - ↑f k) < ε
-- Init.System.IO
IO.Process.StdioConfig.mk.inj : ∀ {stdin stdout stderr stdin_1 stdout_1 stderr_1 : IO.Process.Stdio},
  { stdin := stdin, stdout := stdout, stderr := stderr } =
      { stdin := stdin_1, stdout := stdout_1, stderr := stderr_1 } →
    stdin = stdin_1 ∧ stdout = stdout_1 ∧ stderr = stderr_1
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.X_pow_eq_monomial : ∀ {R : Type u} {σ : Type u_1} {e : ℕ} {n : σ} [inst : CommSemiring R],
  MvPolynomial.X n ^ e = (MvPolynomial.monomial fun₀ | n => e) 1
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- `p` is a Taylor series of `f` up to `n+1` if and only if `p.shift` is a Taylor series up to `n`
for `p 1`, which is a derivative of `f`.  -/
hasFTaylorSeriesUpTo_succ_nat_iff_right : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : E → FormalMultilinearSeries 𝕜 E F} {n : ℕ},
  HasFTaylorSeriesUpTo (↑(n + 1)) f p ↔
    (∀ (x : E), (p x 0).curry0 = f x) ∧
      (∀ (x : E), HasFDerivAt (fun y => p y 0) (p x 1).curryLeft x) ∧
        HasFTaylorSeriesUpTo (↑n) (fun x => (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) fun x => (p x).shift
-- Mathlib.Topology.Connected.PathConnected
/-- Any two points in a path-connected space must be joined by a continuous path.  -/
PathConnectedSpace.joined : ∀ {X : Type u_4} {inst : TopologicalSpace X} [self : PathConnectedSpace X] (x y : X), Joined x y
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- Suppose that a function `f : ℂ → E` is continuous on a closed rectangle with opposite corners at
`z w : ℂ`, is *real* differentiable on the corresponding open rectangle, and
$\frac{\partial f}{\partial \bar z}$ is integrable on this rectangle. Then the integral of `f` over
the boundary of the rectangle is equal to the integral of
$2i\frac{\partial f}{\partial \bar z}=i\frac{\partial f}{\partial x}-\frac{\partial f}{\partial y}$
over the rectangle.  -/
Complex.integral_boundary_rect_of_continuousOn_of_hasFDerivAt_real : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℂ → E) (f' : ℂ → ℂ →L[ℝ] E) (z w : ℂ),
  ContinuousOn f (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im) →
    (∀ x ∈ Set.Ioo (min z.re w.re) (max z.re w.re) ×ℂ Set.Ioo (min z.im w.im) (max z.im w.im), HasFDerivAt f (f' x) x) →
      MeasureTheory.IntegrableOn (fun z => Complex.I • (f' z) 1 - (f' z) Complex.I)
          (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im) MeasureTheory.volume →
        (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * Complex.I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * Complex.I)) +
              Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * Complex.I)) -
            Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * Complex.I) =
          ∫ (x : ℝ) in z.re..w.re,
            ∫ (y : ℝ) in z.im..w.im, Complex.I • (f' (↑x + ↑y * Complex.I)) 1 - (f' (↑x + ↑y * Complex.I)) Complex.I
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.size_alter_eq_add_one : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β},
  k ∉ t → (f (Std.DTreeMap.Const.get? t k)).isSome = true → (Std.DTreeMap.Const.alter t k f).size = t.size + 1
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
/-- Division preserves finiteness.  -/
Set.fintypeDiv : {α : Type u_2} → [inst : Div α] → [DecidableEq α] → (s t : Set α) → [Fintype ↑s] → [Fintype ↑t] → Fintype ↑(s / t)