mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Congruence.Basic
/-- The second isomorphism theorem for `AddMonoid`s.  -/
AddCon.comapQuotientEquiv : {M : Type u_1} →
  {N : Type u_2} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass N] →
        (c : AddCon M) → (f : N →+ M) → (AddCon.comap ⇑f ⋯ c).Quotient ≃+ ↥(AddMonoidHom.mrange (c.mk'.comp f))
-- Mathlib.Algebra.Algebra.Unitization
/-- The star algebra equivalence obtained by restricting `Unitization.inrNonUnitalStarAlgHom`
to its range.  -/
Unitization.inrRangeEquiv : (R : Type u_1) →
  (A : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : StarAddMonoid R] →
        [inst_2 : NonUnitalSemiring A] →
          [inst_3 : Star A] →
            [inst_4 : Module R A] →
              [inst_5 : IsScalarTower R A A] →
                [inst_6 : SMulCommClass R A A] →
                  A ≃⋆ₐ[R] ↥(NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom R A))
-- Mathlib.Data.Complex.Basic
/-- This shortcut instance ensures we do not find `NonUnitalCommRing` via the noncomputable
`instCommCStarAlgebraComplex` instance.  -/
Complex.instNonUnitalCommRing : NonUnitalCommRing ℂ
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Sections
CategoryTheory.Over.sectionsUncurry_sectionsCurry : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {I : C} [inst_2 : CategoryTheory.Closed I]
  [inst_3 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.curryRightUnitorHom I)]
  [inst_4 : CategoryTheory.BraidedCategory C] {X : CategoryTheory.Over I} {A : C}
  {u : (CategoryTheory.toOver I).obj A ⟶ X},
  CategoryTheory.Over.sectionsUncurry (CategoryTheory.Over.sectionsCurry u) = u
-- Std.Do.Triple.SpecLemmas
_private.Std.Do.Triple.SpecLemmas.0.Std.Do.WhileVariant.eval_total : ∀ {α : Type u} {ps : Std.Do.PostShape} {P : Std.Do.SPred ps.args} (variant : Std.Do.WhileVariant α ps) (a : α),
  P ⊢ₛ ∃ m, variant.eval a m
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.instInfFiniteIndexNormalSubgroup : {G : Type u_1} → [inst : Group G] → Min (FiniteIndexNormalSubgroup G)
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.ofList : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {l : List ((a : α) × β a)},
  (Std.DHashMap.Raw.ofList l).WF
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.pow_eq_empty : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] {s : Finset α} {n : ℕ}, s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.sdiv_mem_sdiv : ∀ {α : Type u_2} {β : Type u_3} [inst : SDiv α β] {s t : Set β} {b c : β}, b ∈ s → c ∈ t → b /ₛ c ∈ s /ₛ t
-- Lean.CoreM
Lean.DeclNameGenerator.ofPrefix : Lean.Name → Lean.DeclNameGenerator
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.C0.congr_simp : ∀ {I : Type u} (C C_1 : Set (I → Bool)),
  C = C_1 →
    ∀ [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o o_1 : Ordinal.{u}} (e_o : o = o_1)
      (ho : o < Ordinal.type fun x1 x2 => x1 < x2) (a a_1 : I → Bool),
      a = a_1 → Profinite.NobelingProof.C0 C ho a = Profinite.NobelingProof.C0 C_1 ⋯ a_1
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.restrict_indep_iff : ∀ {α : Type u_1} {M : Matroid α} {R I : Set α}, (M.restrict R).Indep I ↔ M.Indep I ∧ I ⊆ R
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.isoClosure_strictMap_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (P : CategoryTheory.MorphismProperty C) (F : CategoryTheory.Functor C D),
  P.isoClosure.strictMap F ≤ (P.strictMap F).isoClosure
-- Mathlib.Data.Finsupp.Option
Finsupp.some_single_some : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (a : α) (m : M), (fun₀ | some a => m).some = fun₀ | a => m
-- Mathlib.Topology.Closure
IsClosed.mem_iff_closure_subset : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s : Set X}, IsClosed s → (x ∈ s ↔ closure {x} ⊆ s)
-- Init.Data.UInt.Lemmas
USize.toUInt8_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toUInt8 = OfNat.ofNat n
-- Mathlib.Algebra.Algebra.Bilinear
/-- The multiplication map on a non-unital algebra, as an `R`-linear map from `A ⊗[R] A` to `A`.  -/
RingTheory.LinearMap.termμ : Lean.ParserDescr
-- Std.Data.ExtTreeSet.Basic
Std.ExtTreeSet.instForMOfTransCmpOfLawfulMonad : {α : Type u} →
  {cmp : α → α → Ordering} →
    {m : Type w → Type w₂} → [Std.TransCmp cmp] → [inst : Monad m] → [LawfulMonad m] → ForM m (Std.ExtTreeSet α cmp) α
-- Mathlib.NumberTheory.NumberField.Discriminant.Basic
NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  MeasureTheory.volume (ZSpan.fundamentalDomain (NumberField.mixedEmbedding.latticeBasis K)) =
    2⁻¹ ^ NumberField.InfinitePlace.nrComplexPlaces K * ↑(NNReal.sqrt ‖NumberField.discr K‖₊)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- The pushforward of a vector measure along a function.  -/
MeasureTheory.VectorMeasure.map : {α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} →
      [inst : MeasurableSpace β] →
        {M : Type u_3} →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : TopologicalSpace M] → MeasureTheory.VectorMeasure α M → (α → β) → MeasureTheory.VectorMeasure β M
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.isUniformEmbedding_postcomp : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂]
  [inst_2 : NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [inst_3 : RingHomCompTriple σ τ ρ]
  {E : Type u_4} {F : Type u_5} {G : Type u_6} [inst_4 : AddCommGroup E] [inst_5 : Module 𝕜₁ E]
  [inst_6 : AddCommGroup F] [inst_7 : Module 𝕜₂ F] [inst_8 : AddCommGroup G] [inst_9 : Module 𝕜₃ G]
  [inst_10 : TopologicalSpace E] [inst_11 : UniformSpace F] [inst_12 : IsUniformAddGroup F] [inst_13 : UniformSpace G]
  [inst_14 : IsUniformAddGroup G] (f : F →SL[τ] G), IsUniformEmbedding ⇑f → IsUniformEmbedding f.comp
-- Mathlib.Topology.Connected.PathConnected
/-- If `h : X → Y` is a homeomorphism, `h⁻¹(s)` is path-connected iff `s` is.  -/
Homeomorph.isPathConnected_preimage : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set Y} (h : X ≃ₜ Y),
  IsPathConnected (⇑h ⁻¹' s) ↔ IsPathConnected s
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.addMap_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 →
          ¬(P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 ∧ P 1 * Q 2 ^ 3 = W.negY Q * P 2 ^ 3) →
            W.addMap ⟦P⟧ ⟦Q⟧ =
              ⟦![W.toAffine.addX (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2)
                    (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)),
                  W.toAffine.addY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3)
                    (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3)),
                  1]⟧
-- Mathlib.Data.Finmap
Finmap.insert_union : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a} {s₁ s₂ : Finmap β},
  Finmap.insert a b (s₁ ∪ s₂) = Finmap.insert a b s₁ ∪ s₂
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
rank_span_set : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {s : Set M}, LinearIndepOn R id s → Module.rank R ↥(Submodule.span R s) = Cardinal.mk ↑s
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- A correspondence `f : α → Set β` is lower hemicontinuous if and only if its *upper inverse*
(i.e., `u : Set β ↦ f ⁻¹' (Iic u)`, note that `f ⁻¹' (Iic u) = {x | f x ⊆ u}`) sends closed sets
to closed sets.  -/
lowerHemicontinuous_iff_isClosed_preimage_Iic : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β} [inst_1 : TopologicalSpace β],
  LowerHemicontinuous f ↔ ∀ (u : Set β), IsClosed u → IsClosed (f ⁻¹' Set.Iic u)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.isHashSelf_updateBucket_alter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] [inst_2 : Hashable α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α fun x => β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {f : Option β → Option β},
      Std.DHashMap.Internal.IsHashSelf
        (Std.DHashMap.Internal.updateBucket (↑m).buckets ⋯ a (Std.DHashMap.Internal.AssocList.Const.alter a f))
-- Mathlib.Algebra.Group.Subsemigroup.Operations
MulHom.codRestrict.eq_1 : ∀ {M : Type u_1} {N : Type u_2} {σ : Type u_4} [inst : Mul M] [inst_1 : Mul N] [inst_2 : SetLike σ N]
  [inst_3 : MulMemClass σ N] (f : M →ₙ* N) (S : σ) (h : ∀ (x : M), f x ∈ S),
  f.codRestrict S h = { toFun := fun n => ⟨f n, ⋯⟩, map_mul' := ⋯ }
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey_inter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α} {h_mem : k ∈ t₁ ∩ t₂}, (t₁ ∩ t₂).getKey k h_mem = t₁.getKey k ⋯
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_inter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} [inst_2 : Inhabited β], (m₁ ∩ m₂)[k]! = if k ∈ m₂ then m₁[k]! else default
-- Mathlib.Order.Partition.Finpartition
Finpartition.ofPairwiseDisjoint.congr_simp : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : OrderBot α] [inst_2 : DecidableEq α] (parts : Finset α)
  (hdisjoint : (↑parts).PairwiseDisjoint id),
  Finpartition.ofPairwiseDisjoint parts hdisjoint = Finpartition.ofPairwiseDisjoint parts hdisjoint
-- Mathlib.LinearAlgebra.InvariantBasisNumber
RankCondition.mk : ∀ {R : Type u} [inst : Semiring R],
  (∀ {n m : ℕ} (f : (Fin n → R) →ₗ[R] Fin m → R), Function.Surjective ⇑f → m ≤ n) → RankCondition R
-- Mathlib.RingTheory.Localization.Submodule
IsLocalization.coeSubmodule_top : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
  IsLocalization.coeSubmodule S ⊤ = 1
-- Mathlib.MeasureTheory.Measure.FiniteMeasureProd
MeasureTheory.ProbabilityMeasure.prod_apply_symm : ∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_2} [inst_1 : MeasurableSpace β]
  (μ : MeasureTheory.ProbabilityMeasure α) (ν : MeasureTheory.ProbabilityMeasure β) (s : Set (α × β)),
  MeasurableSet s → (μ.prod ν) s = (∫⁻ (y : β), ↑μ ((fun x => (x, y)) ⁻¹' s) ∂↑ν).toNNReal
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.inc.inj : ∀ {x : Lean.IR.VarId} {n : ℕ} {c persistent : Bool} {b : Lean.IR.FnBody} {x_1 : Lean.IR.VarId} {n_1 : ℕ}
  {c_1 persistent_1 : Bool} {b_1 : Lean.IR.FnBody},
  Lean.IR.FnBody.inc x n c persistent b = Lean.IR.FnBody.inc x_1 n_1 c_1 persistent_1 b_1 →
    x = x_1 ∧ n = n_1 ∧ c = c_1 ∧ persistent = persistent_1 ∧ b = b_1
-- Mathlib.Data.Matrix.Basic
Matrix.piEquiv_symm_apply : ∀ {m : Type u_2} {n : Type u_3} {ι : Type u_14} {β : ι → Type u_15} (f : (i : ι) → Matrix m n (β i)),
  Matrix.piEquiv.symm f = Matrix.of fun j k i => f i j k
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
ClosedSubmodule.mulI_mulI_eq : ∀ {H : Type u_1} [inst : NormedAddCommGroup H] [ipc : InnerProductSpace ℂ H] (S : ClosedSubmodule ℝ H), S.mulI.mulI = S
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.IsPresentation.linearEquiv.congr_simp : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] {solution solution_1 : relations.Solution M} (e_solution : solution = solution_1)
  (h : solution.IsPresentation), h.linearEquiv = ⋯.linearEquiv
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type that satisfies `(f + g) x = f x + g x`, `0 x = 0`, and
`(n • f) x = n • f x` is a cancel commutative additive monoid if `β` is a cancel commutative
additive monoid.  -/
FunLike.addCancelCommMonoid : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Add F] →
          [inst_2 : Zero F] →
            [inst_3 : SMul ℕ F] →
              [inst_4 : AddCancelCommMonoid β] →
                [IsZeroApply F α β] → [IsAddApply F α β] → [IsSMulApply ℕ F α β] → AddCancelCommMonoid F
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- The additive closure of a submonoid is a subsemiring.  -/
Submonoid.subsemiringClosure : {R : Type u} → [inst : NonAssocSemiring R] → Submonoid R → Subsemiring R
-- Mathlib.Order.Interval.Set.OrderIso
/-- Order isomorphism between `Iic (⊤ : α)` and `α` when `α` has a top element  -/
OrderIso.IicTop : {α : Type u_1} → [inst : Preorder α] → [inst_1 : OrderTop α] → ↑(Set.Iic ⊤) ≃o α
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Valuation.toTopologicalSpace_eq : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [_t : TopologicalSpace R] [IsValuativeTopology R] (v : Valuation R Γ₀) [v.Compatible], _t = ⋯.topology
-- Mathlib.Algebra.Pointwise.Stabilizer
AddAction.mem_stabilizer_finset_iff_vadd_finset_subset : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] {a : G} [inst_2 : DecidableEq α]
  {s : Finset α}, a ∈ AddAction.stabilizer G s ↔ a +ᵥ s ⊆ s
-- Std.Sat.AIG.If
Std.Sat.AIG.mkIfCached.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (input : aig.TernaryInput),
  aig.mkIfCached input =
    (((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached (input.cast ⋯).discr).aig.mkAndCached
            {
              lhs :=
                ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached (input.cast ⋯).discr).ref,
              rhs := ((input.cast ⋯).cast ⋯).rhs }).aig.mkOrCached
      { lhs := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).ref.cast ⋯,
        rhs :=
          (((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
                    (input.cast ⋯).discr).aig.mkAndCached
              {
                lhs :=
                  ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached (input.cast ⋯).discr).ref,
                rhs := ((input.cast ⋯).cast ⋯).rhs }).ref }
-- Mathlib.LinearAlgebra.Charpoly.ToMatrix
LinearEquiv.charpoly_conj : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M₁] [inst_2 : Module R M₁]
  [inst_3 : Module.Finite R M₁] [inst_4 : Module.Free R M₁] [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂]
  [inst_7 : Module.Finite R M₂] [inst_8 : Module.Free R M₂] (e : M₁ ≃ₗ[R] M₂) (φ : Module.End R M₁),
  LinearMap.charpoly (e.conj φ) = LinearMap.charpoly φ
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.Additive] (n : ℤ),
  CategoryTheory.Functor.commShiftIso (F.mapHomologicalComplex (ComplexShape.up ℤ)) n = F.mapCochainComplexShiftIso n
-- Mathlib.Algebra.Group.Defs
Group.toDivisionMonoid.eq_1 : ∀ {G : Type u_1} [inst : Group G],
  Group.toDivisionMonoid = { toDivInvMonoid := inst.toDivInvMonoid, inv_inv := ⋯, mul_inv_rev := ⋯, inv_eq_of_mul := ⋯ }
-- Lean.Meta.Tactic.Grind.AC.Seq
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.StartsWithResult.prefix.injEq : ∀ (s s_1 : Lean.Grind.AC.Seq),
  (Lean.Grind.AC.StartsWithResult.prefix✝ s = Lean.Grind.AC.StartsWithResult.prefix✝ s_1) = (s = s_1)
-- Init.Data.SInt.Lemmas
Int32.toInt8_sub : ∀ (a b : Int32), (a - b).toInt8 = a.toInt8 - b.toInt8
-- Mathlib.Topology.Instances.CantorSet
/-- The ternary Cantor set is a subset of [0,1].  -/
cantorSet_subset_unitInterval : cantorSet ⊆ Set.Icc 0 1
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
/-- The fundamental property of the operator norm of a continuous alternating map:
`‖f m‖` is bounded by `‖f‖` times the product of the `‖m i‖`.  -/
ContinuousAlternatingMap.le_opNorm : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] (f : E [⋀^ι]→L[𝕜] F) (m : ι → E), ‖f m‖ ≤ ‖f‖ * ∏ i, ‖m i‖
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_modify_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] [inst_1 : Inhabited α] {k : α} {f : β k → β k},
  (t.modify k f).getKey! k = if k ∈ t then k else default
-- Mathlib.Computability.Language
instReprSymbol : {T : Type u_4} → {N : Type u_5} → [Repr T] → [Repr N] → Repr (Symbol T N)
-- Mathlib.Data.Fintype.Perm
/-- Given a finset, produce the finset of all permutations of its elements.  -/
permsOfFinset : {α : Type u_1} → [DecidableEq α] → Finset α → Finset (Equiv.Perm α)
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.instSMulNatHom : {R : Type u} → [inst : Semiring R] → {M N : SemimoduleCat R} → SMul ℕ (M ⟶ N)
-- Mathlib.MeasureTheory.Function.ConvergenceInDistribution
MeasureTheory.TendstoInDistribution.forall_aemeasurable : ∀ {ι : Type u_1} {E : Type u_2} {Ω' : Type u_3} {Ω : ι → Type u_5} {m : (i : ι) → MeasurableSpace (Ω i)}
  {m' : MeasurableSpace Ω'} {mE : MeasurableSpace E} [inst : TopologicalSpace E] [inst_1 : OpensMeasurableSpace E]
  {X : (i : ι) → Ω i → E} {l : Filter ι} {Z : Ω' → E} {μ : (i : ι) → MeasureTheory.Measure (Ω i)}
  [inst_2 : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)]
  {μ' : autoParam (MeasureTheory.Measure Ω') MeasureTheory.TendstoInDistribution._auto_1}
  [inst_3 : MeasureTheory.IsProbabilityMeasure μ'],
  MeasureTheory.TendstoInDistribution X l Z μ μ' → ∀ (i : ι), AEMeasurable (X i) (μ i)
-- Mathlib.Algebra.Torsor.Defs
Equiv.pointReflection_involutive : ∀ {G : Type u_3} {P : Type u_4} [inst : AddGroup G] [inst_1 : AddTorsor G P] (x : P),
  Function.Involutive ⇑(Equiv.pointReflection x)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
_private.Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme.0.AlgebraicGeometry.Scheme.IdealSheafData.glueDataT'Aux_fst_assoc : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U V W U₀ : ↑X.affineOpens) (hU₀ : ↑U ⊓ ↑W ≤ ↑U₀)
  {Z : AlgebraicGeometry.Scheme} (h : I.glueDataObj V ⟶ Z),
  CategoryTheory.CategoryStruct.comp (I.glueDataT'Aux U V W U₀ hU₀)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯)) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯))
        (CategoryTheory.Limits.pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)))
      (CategoryTheory.CategoryStruct.comp (I.glueDataT U V)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯)) h))
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.AddValuation.map_add : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (x y : ℚ_[p]), min x.addValuationDef y.addValuationDef ≤ (x + y).addValuationDef
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_add_intCast : ∀ {x : ℝ}, x ≠ 0 → ∀ (y : ℝ) (n : ℤ), x ^ (y + ↑n) = x ^ y * x ^ n
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.restrict_apply_measure : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (A : Set Ω) {s : Set Ω},
  MeasurableSet s → ↑(μ.restrict A) s = ↑μ (s ∩ A)
-- Mathlib.Algebra.Group.End
/-- Right-multiplying a permutation with `swap i j` twice gives the original permutation.

This specialization of `swap_mul_self` is useful when using cosets of permutations.
 -/
Equiv.mul_swap_mul_self : ∀ {α : Type u_4} [inst : DecidableEq α] (i j : α) (σ : Equiv.Perm α), σ * Equiv.swap i j * Equiv.swap i j = σ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_insert!_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {a fallback : α} {b : β a}, (Std.DTreeMap.Internal.Impl.insert! a b t).getKeyD a fallback = a
-- Aesop.Tree.State
Aesop.GoalRef.markForcedUnprovable : Aesop.GoalRef → BaseIO Unit
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
IsStarNormal.instNonUnitalIsometricContinuousFunctionalCalculus : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A], NonUnitalIsometricContinuousFunctionalCalculus ℂ A IsStarNormal
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.toMultiplicativeBialgEquiv.eq_1 : ∀ (R : Type u_1) (A : Type u_3) (M : Type u_8) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A]
  [inst_3 : AddMonoid M],
  AddMonoidAlgebra.toMultiplicativeBialgEquiv R A M =
    BialgEquiv.ofAlgEquiv (AddMonoidAlgebra.toMultiplicativeAlgEquiv R A M) ⋯ ⋯
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.inv_subset_closure : ∀ {G : Type u_2} [inst : Group G] (S : Set G), S⁻¹ ⊆ ↑(Subgroup.closure S)
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
/-- `restrictScalars S` is an embedding of the lattice of `R`-submodules into
the lattice of `S`-submodules.  -/
Submodule.restrictScalarsEmbedding : (S : Type u_1) →
  (R : Type u_2) →
    (M : Type u_3) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Semiring S] →
            [inst_3 : Module S M] →
              [inst_4 : Module R M] → [inst_5 : SMul S R] → [IsScalarTower S R M] → Submodule R M ↪o Submodule S M
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
_private.Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs.0.Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.destruct.match_1.eq_1 : ∀ {basis_tl : Tactic.ComputeAsymptotics.Basis}
  (motive : Stream'.Seq1 (ℝ × Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl) → Sort u_1) (exp : ℝ)
  (coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl)
  (tl : Stream'.Seq (ℝ × Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl))
  (h_1 :
    (exp : ℝ) →
      (coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl) →
        (tl : Stream'.Seq (ℝ × Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl)) → motive ((exp, coef), tl)),
  (match ((exp, coef), tl) with
    | ((exp, coef), tl) => h_1 exp coef tl) =
    h_1 exp coef tl
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.instFibrationPResolutionObj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] (X : C),
  HomotopicalAlgebra.Fibration (HomotopicalAlgebra.CofibrantObject.HoCat.pResolutionObj X)
-- Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Ring.HasFiniteQuotients.mk : ∀ {R : Type u_1} [inst : CommRing R], (∀ {I : Ideal R}, I ≠ ⊥ → Finite (R ⧸ I)) → Ring.HasFiniteQuotients R
-- Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
/-- If the maximal spectrum of a ring is a singleton, then the ring is local.  -/
IsLocalRing.of_singleton_maximalSpectrum : ∀ {R : Type u_1} [inst : CommSemiring R] [Subsingleton (MaximalSpectrum R)] [Nonempty (MaximalSpectrum R)],
  IsLocalRing R
-- Init.Data.String.Lemmas.Iterate
String.Pos.Splits.mem_toList_left_iff : ∀ {s : String} {pos : s.Pos} {t u : String} {c : Char},
  pos.Splits t u → (c ∈ t.toList ↔ ∃ pos', ∃ (h : pos' < pos), pos'.get ⋯ = c)
-- Mathlib.RingTheory.Congruence.BigOperators
/-- Congruence relation of a ring preserves finite product.  -/
RingCon.finsetProd : ∀ {ι : Type u_1} {S : Type u_2} [inst : Add S] [inst_1 : CommMonoid S] (t : RingCon S) (s : Finset ι) {f g : ι → S},
  (∀ i ∈ s, t (f i) (g i)) → t (s.prod f) (s.prod g)