mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.DedekindDomain.Different
FractionalIdeal.smul_mem_dual_one : ∀ (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_5) [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [inst_11 : IsDomain A]
  [inst_12 : IsFractionRing A K] [inst_13 : FiniteDimensional K L] [inst_14 : Algebra.IsSeparable K L]
  [inst_15 : IsIntegralClosure B A L] [inst_16 : IsFractionRing B L] [inst_17 : IsIntegrallyClosed A]
  [inst_18 : IsDedekindDomain B] (C : Type u_3) (M : Type u_4) [inst_19 : CommRing C] [inst_20 : IsDedekindDomain C]
  [inst_21 : Field M] [inst_22 : Algebra C M] [inst_23 : IsFractionRing C M] [inst_24 : Algebra A C]
  [inst_25 : Algebra B C] [inst_26 : Algebra A M] [inst_27 : Algebra B M] [inst_28 : Algebra K M]
  [inst_29 : Algebra L M] [inst_30 : IsScalarTower A C M] [inst_31 : IsScalarTower A K M]
  [inst_32 : IsScalarTower B C M] [inst_33 : IsScalarTower B L M] [IsScalarTower K L M]
  [inst_35 : IsIntegralClosure C A M] [inst_36 : FiniteDimensional K M] [inst_37 : FiniteDimensional L M]
  [inst_38 : Algebra.IsSeparable K M] [inst_39 : IsIntegralClosure C B M] [inst_40 : Algebra.IsSeparable L M] {x : L},
  x ∈ FractionalIdeal.dual A K ⋯ → ∀ {y : M}, ⋯ → ⋯
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.instPartialOrder : (R : Type u_1) → [inst : CommRing R] → PartialOrder (RingPreordering R)
-- Mathlib.SetTheory.Cardinal.Ordinal
/-- Bounds the cardinal of an ordinal-indexed union of sets.  -/
Cardinal.mk_biUnion_le_of_le_lift : ∀ {β : Type v} {o : Ordinal.{u}} {c : Cardinal.{v}},
  Cardinal.lift.{v, u} o.card ≤ Cardinal.lift.{u, v} c →
    Cardinal.aleph0 ≤ c →
      ∀ (A : Ordinal.{u} → Set β), (∀ j < o, Cardinal.mk ↑(A j) ≤ c) → Cardinal.mk ↑(⋃ j, ⋃ (_ : j < o), A j) ≤ c
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_diff_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∈ m₂ → (m₁ \ m₂)[k]? = none
-- Init.SimpLemmas
Or.imp_left : ∀ {a b c : Prop}, (a → b) → a ∨ c → b ∨ c
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.IsRankOneDiscrete.valueGroup_genLTOne_eq_generator : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : Ring A] (v : Valuation A Γ)
  [inst_2 : v.IsRankOneDiscrete],
  LinearOrderedCommGroup.Subgroup.genLTOne (MonoidWithZeroHom.ofClass v).valueGroup =
    Valuation.IsRankOneDiscrete.generator v
-- Lean.Data.PersistentHashSet
Lean.PersistentHashSet.set : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.PersistentHashSet α → Lean.PersistentHashMap α Unit
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.SurjectiveOfEpiAuxs.mul_smul : ∀ {A B : GrpCat} (f : A ⟶ B) (b b' : ↑B) (x : GrpCat.SurjectiveOfEpiAuxs.XWithInfinity f), (b * b') • x = b • b' • x
-- Mathlib.Data.Finset.Card
Finset.image_eq_iff_bijOn_of_card : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → β} {t : Finset β} [inst : DecidableEq β],
  s.card ≤ t.card → (Finset.image f s = t ↔ Set.BijOn f ↑s ↑t)
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.IsComplete.completeOn : ∀ {α : Type u_1} (f : Set α), (Hypergraph.completeOn f).IsComplete
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.fderivCompContinuousLinearMap.eq_1 : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : Fintype ι]
  [inst_8 : DecidableEq ι] (f : F [⋀^ι]→L[𝕜] G) (g : E →L[𝕜] F),
  f.fderivCompContinuousLinearMap g =
    ContinuousAlternatingMap.liftCLM
      ((f.fderivCompContinuousLinearMap fun x => g) ∘SL
        ContinuousLinearMap.pi fun x => ContinuousLinearMap.id 𝕜 (E →L[𝕜] F))
      ⋯
-- Mathlib.Data.EReal.Operations
EReal.mul_eq_top : ∀ (a b : EReal), a * b = ⊤ ↔ a = ⊥ ∧ b < 0 ∨ a < 0 ∧ b = ⊥ ∨ a = ⊤ ∧ 0 < b ∨ 0 < a ∧ b = ⊤
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.limitsOfShape_eq_unop_colimitsOfShape : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J], P.limitsOfShape J = (P.op.colimitsOfShape Jᵒᵖ).unop
-- Mathlib.Data.List.Sort
/-- **Alias** of the forward direction of `List.sortedLE_iff_getElem_le_getElem_of_le`. -/
List.SortedLE.getElem_le_getElem_of_le : ∀ {α : Type u_1} {l : List α} [inst : Preorder α],
  l.SortedLE → ∀ ⦃i j : ℕ⦄ ⦃hi : i < l.length⦄ ⦃hj : j < l.length⦄, i ≤ j → l[i] ≤ l[j]
-- Mathlib.Order.CompleteLattice.Defs
CompleteLattice.toCompleteSemilatticeInf : {α : Type u_8} → [self : CompleteLattice α] → CompleteSemilatticeInf α
-- Init.Sym.Lemmas
Lean.Sym.Int16.le_eq_false : ∀ (a b : Int16), decide (a ≤ b) = false → (a ≤ b) = False
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.repr_symm_single : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] (b : OrthonormalBasis ι 𝕜 E) (i : ι),
  b.repr.symm (EuclideanSpace.single i 1) = b i
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.addHaarContent_apply : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  (K₀ : TopologicalSpace.PositiveCompacts G) (K : TopologicalSpace.Compacts G),
  (MeasureTheory.Measure.haar.addHaarContent K₀) K =
    ↑(have this := ⟨MeasureTheory.Measure.haar.addCHaar K₀ K, ⋯⟩;
      this)
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.mapDomainLinearEquiv.eq_1 : ∀ (R : Type u_1) (S : Type u_2) {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Module R S] (e : M ≃ N),
  AddMonoidAlgebra.mapDomainLinearEquiv R S e =
    AddMonoidAlgebra.coeffLinearEquiv R ≪≫ₗ (Finsupp.domLCongr e ≪≫ₗ (AddMonoidAlgebra.coeffLinearEquiv R).symm)
-- Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
LinearMap.GeneralLinearGroup.ofLinearEquiv_mul : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (f g : M ≃ₗ[R] M),
  LinearMap.GeneralLinearGroup.ofLinearEquiv (f * g) =
    LinearMap.GeneralLinearGroup.ofLinearEquiv f * LinearMap.GeneralLinearGroup.ofLinearEquiv g
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The L-series of a Dirichlet character `χ` and of the twist of `μ` by `χ` are multiplicative
inverses.  -/
DirichletCharacter.LSeries.mul_mu_eq_one : ∀ {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ},
  1 < s.re → LSeries (fun n => χ ↑n) s * LSeries ((fun n => χ ↑n) * fun n => ↑(ArithmeticFunction.moebius n)) s = 1
-- Mathlib.Logic.Encodable.Lattice
Encodable.iUnion_decode₂_disjoint_on : ∀ {α : Type u_1} {β : Type u_2} [inst : Encodable β] {f : β → Set α},
  Pairwise (Function.onFun Disjoint f) → Pairwise (Function.onFun Disjoint fun i => ⋃ b ∈ Encodable.decode₂ β i, f b)
-- Mathlib.Computability.Primrec.List
Primrec.list_reverse : ∀ {α : Type u_1} [inst : Primcodable α], Primrec List.reverse
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
CongruenceSubgroup.Gamma1.eq_1 : ∀ (N : ℕ),
  CongruenceSubgroup.Gamma1 N =
    Subgroup.map ((CongruenceSubgroup.Gamma0 N).subtype.comp (CongruenceSubgroup.Gamma1' N).subtype) ⊤
-- Mathlib.Data.Part
Part.eq_none_or_eq_some : ∀ {α : Type u_1} (o : Part α), o = Part.none ∨ ∃ x, o = Part.some x
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.addNegAssignment.eq_4 : Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned.addNegAssignment =
  Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg
-- Mathlib.CategoryTheory.Limits.Connected
CategoryTheory.Limits.isColimitConstCocone.congr_simp : ∀ (J : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  (X : C) [inst_2 : CategoryTheory.IsConnected J],
  CategoryTheory.Limits.isColimitConstCocone J X = CategoryTheory.Limits.isColimitConstCocone J X
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sin_eq_iff_coe_eq_or_add_eq_pi : ∀ {θ ψ : ℝ}, Real.sin θ = Real.sin ψ ↔ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑Real.pi
-- Init.Control.Lawful.MonadLift.Lemmas
liftM_map : ∀ {m : Type u → Type v} {n : Type u → Type w} [inst : Monad m] [inst_1 : Monad n] [inst_2 : MonadLiftT m n]
  [LawfulMonadLiftT m n] {α β : Type u} [LawfulMonad m] [LawfulMonad n] (f : α → β) (ma : m α),
  liftM (f <$> ma) = f <$> liftM ma
-- Mathlib.Topology.Irreducible
isIrreducible_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X}, IsIrreducible {x}
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Prequotient.of.inj : ∀ {J : Type v} {inst : CategoryTheory.Category.{u, v} J} {F : CategoryTheory.Functor J MonCat} {j : J} {x : ↑(F.obj j)}
  {j_1 : J} {x_1 : ↑(F.obj j_1)},
  MonCat.Colimits.Prequotient.of j x = MonCat.Colimits.Prequotient.of j_1 x_1 → j = j_1 ∧ x ≍ x_1
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_one_add_X_pow : ∀ (R : Type u_1) [inst : Semiring R] (n k : ℕ), ((1 + Polynomial.X) ^ n).coeff k = ↑(n.choose k)
-- Mathlib.Analysis.Calculus.FDeriv.Const
differentiableOn_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {s : Set E} (c : F), DifferentiableOn 𝕜 (fun x => c) s
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.gate.inj : ∀ {α : Type} {a : Std.Tactic.BVDecide.Gate} {a_1 a_2 : Std.Tactic.BVDecide.BoolExpr α} {a_3 : Std.Tactic.BVDecide.Gate}
  {a_4 a_5 : Std.Tactic.BVDecide.BoolExpr α},
  Std.Tactic.BVDecide.BoolExpr.gate a a_1 a_2 = Std.Tactic.BVDecide.BoolExpr.gate a_3 a_4 a_5 →
    a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.resolvent_zero_of_mem_spectrum : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {r : R} {a : A},
  r ∈ spectrum R a → resolvent a r = 0
-- Mathlib.Algebra.NoZeroSMulDivisors.Defs
NoZeroDivisors.toNoZeroSMulDivisors : ∀ {R : Type u_1} [inst : Zero R] [inst_1 : Mul R] [NoZeroDivisors R], NoZeroSMulDivisors R R
-- Lean.Data.NameMap.Basic
Lean.NameHashSet.empty : Lean.NameHashSet
-- Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Unitary.openPartialHomeomorph_symm_apply : ∀ {A : Type u_1} [inst : CStarAlgebra A] (a : ↥(selfAdjoint A)),
  ↑Unitary.openPartialHomeomorph.symm a = selfAdjoint.expUnitary a
-- Mathlib.RingTheory.Spectrum.Prime.Topology
/-- The closed point in the prime spectrum of a local ring.  -/
IsLocalRing.closedPoint : (R : Type u) → [inst : CommSemiring R] → [IsLocalRing R] → PrimeSpectrum R
-- Mathlib.CategoryTheory.Action.Limits
/-- `F : C ⥤ Action V G` preserves colimits of some shape `J`
if it does after postcomposing with the forgetful functor `Action V G ⥤ V`.  -/
Action.preservesColimitsOfShape_of_preserves : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {C : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_2, u_3} C] (F : CategoryTheory.Functor C (Action V G)) {J : Type u_4}
  [inst_3 : CategoryTheory.Category.{v_3, u_4} J],
  CategoryTheory.Limits.PreservesColimitsOfShape J (F.comp (Action.forget V G)) →
    CategoryTheory.Limits.PreservesColimitsOfShape J F
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
extChartAt_mem_closure_interior : ∀ {𝕜 : 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]
  {I : ModelWithCorners 𝕜 E H} {s : Set M} [inst_5 : ChartedSpace H M] {x₀ x : M},
  x ∈ closure (interior s) →
    x ∈ (extChartAt I x₀).source →
      ↑(extChartAt I x₀) x ∈ closure (interior (↑(extChartAt I x₀).symm ⁻¹' s ∩ (extChartAt I x₀).target))
-- Std.Http.Server.Handler
/-- Builds a `StatelessHandler` from a request function and a failure callback. Useful for
attaching error logging to a handler.
 -/
Std.Http.Server.Handler.withFailure : Std.Http.Server.StatelessHandler → (IO.Error → Std.Async.Async Unit) → Std.Http.Server.StatelessHandler
-- Mathlib.GroupTheory.Finiteness
AddGroup.fg_iff_addSubgroup_fg : ∀ {G : Type u_3} [inst : AddGroup G] (H : AddSubgroup G), AddGroup.FG ↥H ↔ H.FG
-- Lean.Elab.ConfigEval.Basic
/-- Evaluate `stx` using either `evalExpr`.
 -/
Lean.Elab.ConfigEval.evalExprWithElab : {α : Type} → [Lean.Elab.ConfigEval.EvalExpr α] → Lean.Term → Lean.Elab.TermElabM α
-- Init.Data.Int.DivMod.Bootstrap
Int.ediv_mul_cancel : ∀ {a b : ℤ}, b ∣ a → a / b * b = a
-- Mathlib.Algebra.Group.End
Equiv.Perm.refl_mul : ∀ {α : Type u_4} (e : Equiv.Perm α), Equiv.refl α * e = e
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_filterMap : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Inhabited γ] {f : α → β → Option γ} {k : α} (h : t.WF),
  Std.DTreeMap.Raw.Const.get! (Std.DTreeMap.Raw.filterMap f t) k =
    ((Std.DTreeMap.Raw.Const.get? t k).pbind fun x h' => f (t.getKey k ⋯) x).get!
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.FullyFaithful.preimageIso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X Y : C} (e : F.obj X ≅ F.obj Y),
  (hF.preimageIso e).inv = hF.preimage e.inv
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
/-- The short complex `Hⁱ(G, X₃) ⟶ Hʲ(G, X₁) ⟶ Hʲ(G, X₂)` associated to an exact
sequence of representations `0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0`.  -/
groupCohomology.mapShortComplex₁ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)} →
        X.ShortExact → {i j : ℕ} → i + 1 = j → CategoryTheory.ShortComplex (ModuleCat k)
-- Mathlib.Order.SuccPred.IntervalSucc
/-- Special case `a = ⊥` of `biUnion_Ici_Ico_map_succ`.  -/
iUnion_Ico_map_succ_eq_Ici : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : OrderBot α] [inst_2 : SuccOrder α]
  [IsSuccArchimedean α] [inst_4 : LinearOrder β] {f : α → β},
  (∀ (a : α), f ⊥ ≤ f a) → ¬BddAbove (Set.range f) → ⋃ a, Set.Ico (f a) (f (Order.succ a)) = Set.Ici (f ⊥)
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.map_sup : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] {f : L →ₗ⁅R⁆ L'} {I I₂ : LieIdeal R L},
  LieIdeal.map f (I ⊔ I₂) = LieIdeal.map f I ⊔ LieIdeal.map f I₂
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
/-- Construct a modification isomorphism between oplax natural transformations
by giving object level isomorphisms, and checking naturality only in the forward direction.
 -/
CategoryTheory.Oplax.OplaxTrans.isoMk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          {η θ : F ⟶ G} →
            (app : (a : B) → η.app a ≅ θ.app a) →
              autoParam
                  (∀ {a b : B} (f : a ⟶ b),
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b).hom)
                        (θ.naturality f) =
                      CategoryTheory.CategoryStruct.comp (η.naturality f)
                        (CategoryTheory.Bicategory.whiskerRight (app a).hom (G.map f)))
                  CategoryTheory.Oplax.OplaxTrans.isoMk._auto_1 →
                (η ≅ θ)
-- Mathlib.Data.Sigma.Basic
Prod.toSigma_injective : ∀ {α : Type u_7} {β : Type u_8}, Function.Injective Prod.toSigma
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.ofFaithful.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F} {D : Type u₄}
  [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (G : CategoryTheory.Functor C D) [inst_3 : G.Faithful]
  (ht : CategoryTheory.Limits.IsLimit (G.mapCone t)) (lift : (s : CategoryTheory.Limits.Cone F) → s.pt ⟶ t.pt)
  (h : ∀ (s : CategoryTheory.Limits.Cone F), G.map (lift s) = ht.lift (G.mapCone s)),
  CategoryTheory.Limits.IsLimit.ofFaithful G ht lift h = { lift := lift, fac := ⋯, uniq := ⋯ }
-- Mathlib.Analysis.Calculus.Deriv.AffineMap
AffineMap.derivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (f : 𝕜 →ᵃ[𝕜] E) {s : Set 𝕜} {x : 𝕜},
  UniqueDiffWithinAt 𝕜 s x → derivWithin (⇑f) s x = f.linear 1
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_inter_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∉ m₁ → (m₁ ∩ m₂).getKey? k = none
-- Mathlib.NumberTheory.RamificationInertia.Basic
Ideal.Factors.ramificationIdx_ne_zero : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : IsDedekindDomain S] (P : ↥(UniqueFactorizationMonoid.factors (Ideal.map (algebraMap R S) p)).toFinset),
  p.ramificationIdx' ↑P ≠ 0
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- Given a continuous `AddMonoidHom` `f : M → N`, `mapRangeHom` is the `AddMonoidHom` mapping the
vector measure `v` on `M` to the vector measure `f ∘ v` on `N`.  -/
MeasureTheory.VectorMeasure.mapRangeHom : {M : Type u_3} →
  [inst : AddCommMonoid M] →
    [inst_1 : TopologicalSpace M] →
      {N : Type u_4} →
        [inst_2 : AddCommMonoid N] →
          [inst_3 : TopologicalSpace N] →
            [inst_4 : ContinuousAdd M] →
              [inst_5 : ContinuousAdd N] →
                {α : Type u_5} →
                  [inst_6 : MeasurableSpace α] →
                    (f : M →+ N) → Continuous ⇑f → MeasureTheory.VectorMeasure α M →+ MeasureTheory.VectorMeasure α N
-- Mathlib.RingTheory.Finiteness.Defs
/-- An algebra morphism `A →ₐ[R] B` is finite if it is finite as ring morphism.
In other words, if `B` is finitely generated as `A`-module.  -/
AlgHom.Finite : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing A] →
          [inst_2 : CommRing B] → [inst_3 : Algebra R A] → [inst_4 : Algebra R B] → (A →ₐ[R] B) → Prop
-- Mathlib.Algebra.Free
FreeAddSemigroup.tail_add : ∀ {α : Type u} (x y : FreeAddSemigroup α), (x + y).tail = x.tail ++ y.head :: y.tail
-- Mathlib.Topology.Algebra.GroupWithZero
ContinuousAt.inv₀ : ∀ {α : Type u_1} {G₀ : Type u_3} [inst : Zero G₀] [inst_1 : Inv G₀] [inst_2 : TopologicalSpace G₀] [ContinuousInv₀ G₀]
  {f : α → G₀} {a : α} [inst_4 : TopologicalSpace α], ContinuousAt f a → f a ≠ 0 → ContinuousAt f⁻¹ a
-- Mathlib.Data.Int.ModEq
Int.ModEq.add_left : ∀ {n a b : ℤ} (c : ℤ), a ≡ b [ZMOD n] → c + a ≡ c + b [ZMOD n]
-- Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
FirstOrder.Field.modelField_of_modelACF : ∀ (p : ℕ) (K : Type u_2) [inst : FirstOrder.Language.ring.Structure K] [h : K ⊨ FirstOrder.Language.Theory.ACF p],
  K ⊨ FirstOrder.Language.Theory.field
-- Mathlib.Topology.MetricSpace.Infsep
Set.Nontrivial.infsep_eq_iInf : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {s : Set α}, s.Nontrivial → s.infsep = ⨅ d, Function.uncurry dist ↑d
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- The inclusion homomorphism `N →+ E`  -/
AddGroupExtension.inl : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : AddGroup N] → [inst_1 : AddGroup E] → [inst_2 : AddGroup G] → AddGroupExtension N E G → N →+ E
-- Mathlib.Data.Finset.Insert
Finset.insert_ne_self : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a : α}, insert a s ≠ s ↔ a ∉ s
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivAtFilter_one : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (L : Filter (𝕜 × 𝕜)) [inst_3 : One F], HasDerivAtFilter 1 0 L
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- For `1 ≤ r`, the logarithmic counting function respects the `≤` relation.
 -/
Function.locallyFinsuppWithin.logCounting_le : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : ProperSpace E] {f₁ f₂ : Function.locallyFinsupp E ℤ} {r : ℝ},
  f₁ ≤ f₂ → 1 ≤ r → Function.locallyFinsuppWithin.logCounting f₁ r ≤ Function.locallyFinsuppWithin.logCounting f₂ r
-- Mathlib.Tactic.Simps.Basic
/-- `simpsTac` derives `simp` lemmas for all (nested) non-Prop projections of the declaration.
If `todo` is non-empty, it will generate exactly the names in `todo`.
If `shortNm` is true, the generated names will only use the last projection name.
If `trc` is true, trace as if `trace.simps.verbose` is true.  -/
simpsTac : Lean.Syntax →
  Lean.Name →
    optParam Simps.Config { } →
      optParam (List (String × Lean.Syntax)) [] → optParam Bool false → Lean.AttrM (Array Lean.Name)
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.instInhabitedZoneRules.default : Std.Time.TimeZone.ZoneRules
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
/-- Eta-expanded form of `mvfderivWithin_mul` -/
mvfderivWithin_fun_mul : ∀ {𝕜 : 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] {s : Set M} {f g : M → 𝕜} {x : M},
  MDiffAt[s] f x → MDiffAt[s] g x → UniqueMDiffAt[s] x → (d[s] fun i => f i * g i) x = f x • d[s] g x + g x • d[s] f x
-- Mathlib.Analysis.RCLike.Sqrt
Complex.sqrt.eq_1 : ∀ (a : ℂ), a.sqrt = a ^ 2⁻¹
-- Init.Data.SInt.Basic
Int64.ofUInt64.injEq : ∀ (toUInt64 toUInt64_1 : UInt64), ({ toUInt64 := toUInt64 } = { toUInt64 := toUInt64_1 }) = (toUInt64 = toUInt64_1)
-- Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
CochainComplex.MappingConeCompHomotopyEquiv.hom_inv_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃),
  CategoryTheory.CategoryStruct.comp (CochainComplex.MappingConeCompHomotopyEquiv.hom f g)
      (CochainComplex.MappingConeCompHomotopyEquiv.inv f g) =
    CategoryTheory.CategoryStruct.id (CochainComplex.mappingCone g)
-- Init.Data.List.Attach
List.map_attachWith_eq_pmap : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {P : α → Prop} {H : ∀ a ∈ l, P a} {f : { x // P x } → β},
  List.map f (l.attachWith P H) = List.pmap (fun a h => f ⟨a, ⋯⟩) l ⋯
-- Mathlib.LinearAlgebra.AffineSpace.Pointwise
AffineSubspace.vadd_mem_pointwise_vadd_iff : ∀ {k : Type u_2} {V : Type u_3} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {v : V} {s : AffineSubspace k P} {p : P}, v +ᵥ p ∈ v +ᵥ s ↔ p ∈ s
-- Mathlib.LinearAlgebra.Dimension.Constructions
Module.Basis.sumQuot_repr_inr : ∀ {R : Type u_2} {V : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {W : Submodule R V}
  {m : Type u_4} {n : Type u_5} (bW : Module.Basis m R ↥W) (bQ : Module.Basis n R (V ⧸ W)) (v : V) (j : n),
  ((bW.sumQuot bQ).repr v) (Sum.inr j) = (bQ.repr (W.mkQ v)) j
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.f'_cyclesMap' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData),
  CategoryTheory.CategoryStruct.comp h₁.f' (CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂) =
    CategoryTheory.CategoryStruct.comp φ.τ₁ h₂.f'