mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.EuclideanDomain.Defs
/-- An implementation of the extended GCD algorithm.
At each step we are computing a triple `(r, s, t)`, where `r` is the next value of the GCD
algorithm, to compute the greatest common divisor of the input (say `x` and `y`), and `s` and `t`
are the coefficients in front of `x` and `y` to obtain `r` (i.e. `r = s * x + t * y`).
The function `xgcdAux` takes in two triples, and from these recursively computes the next triple:
```
xgcdAux (r, s, t) (r', s', t') = xgcdAux (r' % r, s' - (r' / r) * s, t' - (r' / r) * t) (r, s, t)
```
 -/
EuclideanDomain.xgcdAux : {R : Type u} → [EuclideanDomain R] → [DecidableEq R] → R → R → R → R → R → R → R × R × R
-- Lean.Meta.Tactic.Grind.Arith.Util
Lean.Meta.Grind.Arith.CollectDecVars.State.found : Lean.Meta.Grind.Arith.CollectDecVars.State → Lean.FVarIdSet
-- Mathlib.Algebra.Order.ToIntervalMod
self_sub_toIocDiv_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R), b - ↑(toIocDiv hp a b) * p = toIocMod hp a b
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.ColimitPresentation.self_diag : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  (CategoryTheory.Limits.ColimitPresentation.self X).diag = (CategoryTheory.Functor.const PUnit.{s + 1}).obj X
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.ofConjAct_one : ∀ {G : Type u_3} [inst : DivInvMonoid G], ConjAct.ofConjAct 1 = 1
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
_private.Mathlib.MeasureTheory.Function.ConvergenceInMeasure.0.MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.pairwise_disjoint_Ioc_mul_zpow : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  Pairwise (Function.onFun Disjoint fun n => Set.Ioc (a * b ^ n) (a * b ^ (n + 1)))
-- Std.Data.Internal.List.Associative
Std.Internal.List.le_maxKeyD_of_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α},
      Std.Internal.List.containsKey k l = true →
        ∀ {fallback : α}, (compare k (Std.Internal.List.maxKeyD l fallback)).isLE = true
-- Init.Data.String.Pattern.String
String.Slice.Pattern.ForwardSliceSearcher.emptyBefore : {s : String.Slice} → s.Pos → String.Slice.Pattern.ForwardSliceSearcher s
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Cofan.IsColimit.inj_desc : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : β → C} {c : CategoryTheory.Limits.Cofan X}
  (d : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c) (i : β),
  CategoryTheory.CategoryStruct.comp (c.inj i) (hc.desc d) = d.inj i
-- Mathlib.AlgebraicGeometry.StructureSheaf
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.germₗ : {R : Type u} →
  (M : Type u) →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) →
            (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) →
              x ∈ U →
                (AlgebraicGeometry.structureSheafInType R M).obj.obj (Opposite.op U) →ₗ[R]
                  ↑(TopCat.Presheaf.stalk (AlgebraicGeometry.moduleStructurePresheaf R M).presheaf x)
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.comp_assoc : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {P : Type u_3} [inst_2 : Monoid P] {φ : M →* N}
  {ψ : N →* P} {χ : M →* P} {A : Type u_4} [inst_3 : AddMonoid A] [inst_4 : DistribMulAction M A] {B : Type u_5}
  [inst_5 : AddMonoid B] [inst_6 : DistribMulAction N B] {C : Type u_7} [inst_7 : AddMonoid C]
  [inst_8 : DistribMulAction P C] {Q : Type u_11} {D : Type u_12} [inst_9 : Monoid Q] [inst_10 : AddMonoid D]
  [inst_11 : DistribMulAction Q D] {η : P →* Q} {θ : M →* Q} {ζ : N →* Q} (h : C →ₑ+[η] D) (g : B →ₑ+[ψ] C)
  (f : A →ₑ+[φ] B) [inst_12 : φ.CompTriple ψ χ] [inst_13 : χ.CompTriple η θ] [inst_14 : ψ.CompTriple η ζ]
  [inst_15 : φ.CompTriple ζ θ], h.comp (g.comp f) = (h.comp g).comp f
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.ι_leftKanExtensionObjIsoColimit_hom : ∀ {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] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] (F : CategoryTheory.Functor C H)
  [inst_3 : L.HasPointwiseLeftKanExtension F] (X : D) (f : CategoryTheory.CostructuredArrow L X),
  CategoryTheory.CategoryStruct.comp ((L.leftKanExtensionUnit F).app f.left)
      (CategoryTheory.CategoryStruct.comp ((L.leftKanExtension F).map f.hom)
        (L.leftKanExtensionObjIsoColimit F X).hom) =
    CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.proj L X).comp F) f
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.lie_mem' : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L]
  (self : LieRinehartSubalgebra A L) {a b : L}, a ∈ self.carrier → b ∈ self.carrier → ⁅a, b⁆ ∈ self.carrier
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_Ioc : ∀ {a b : ℝ}, MeasureTheory.volume (Set.Ioc a b) = ENNReal.ofReal (b - a)
-- Batteries.Data.List.Basic
/-- Check for all elements `a`, `b`, where `a` and `b` are the nth element of the first and second
List respectively, that `r a b = true`.
 -/
List.all₂ : {α : Type u_1} → {β : Type u_2} → (α → β → Bool) → List α → List β → Bool
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- If a linear isometry has an inverse, it is a linear isometric equivalence.  -/
LinearIsometryEquiv.ofLinearIsometry : {R : Type u_1} →
  {R₂ : Type u_2} →
    {E : Type u_5} →
      {E₂ : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            {σ₁₂ : R →+* R₂} →
              {σ₂₁ : R₂ →+* R} →
                [inst_2 : RingHomInvPair σ₁₂ σ₂₁] →
                  [inst_3 : RingHomInvPair σ₂₁ σ₁₂] →
                    [inst_4 : SeminormedAddCommGroup E] →
                      [inst_5 : SeminormedAddCommGroup E₂] →
                        [inst_6 : Module R E] →
                          [inst_7 : Module R₂ E₂] →
                            (f : E →ₛₗᵢ[σ₁₂] E₂) →
                              (g : E₂ →ₛₗ[σ₂₁] E) →
                                f.toLinearMap ∘ₛₗ g = LinearMap.id → g ∘ₛₗ f.toLinearMap = LinearMap.id → E ≃ₛₗᵢ[σ₁₂] E₂
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.IsRingHom.toIsMonHom : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  {R₁ R₂ : C} {inst_2 : CategoryTheory.AddMonObj R₁} {inst_3 : CategoryTheory.AddMonObj R₂}
  {inst_4 : CategoryTheory.MonObj R₁} {inst_5 : CategoryTheory.MonObj R₂} {f : R₁ ⟶ R₂}
  [self : CategoryTheory.IsRingHom f], CategoryTheory.IsMonHom f
-- Mathlib.Algebra.Category.GrpWithZero
GrpWithZero.hasForgetToBipointed : CategoryTheory.HasForget₂ GrpWithZero Bipointed
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
CochainComplex.shiftShortComplexFunctorIso.congr_simp : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (n i i' : ℤ)
  (hi : n + i = i'),
  CochainComplex.shiftShortComplexFunctorIso C n i i' hi = CochainComplex.shiftShortComplexFunctorIso C n i i' hi
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_insertIfNew!_le_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {v : β k} {fallback : α},
      (compare ((Std.DTreeMap.Internal.Impl.insertIfNew! k v t).minKeyD fallback) k).isLE = true
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.endsWith_char_eq_false_iff_forall_append : ∀ {c : Char} {s : String}, s.endsWith c = false ↔ ∀ (t : String), s ≠ t ++ String.singleton c
-- Init.Data.Array.Extract
Array.extract_eq_extract_left : ∀ {α : Type u_1} {as : Array α} {i i' j : ℕ}, as.extract i j = as.extract i' j ↔ min j as.size - i = min j as.size - i'
-- Lean.DocString.Add
Lean.VersoDocResult.mk.injEq : ∀ (toVersoDocString : Lean.VersoDocString) (deferredChecks : Array Lean.Doc.DeferredCheck)
  (toVersoDocString_1 : Lean.VersoDocString) (deferredChecks_1 : Array Lean.Doc.DeferredCheck),
  ({ toVersoDocString := toVersoDocString, deferredChecks := deferredChecks } =
      { toVersoDocString := toVersoDocString_1, deferredChecks := deferredChecks_1 }) =
    (toVersoDocString = toVersoDocString_1 ∧ deferredChecks = deferredChecks_1)
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
CategoryTheory.regularMonoCategoryOfNormalMonoCategory : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.IsNormalMonoCategory C], CategoryTheory.IsRegularMonoCategory C
-- Mathlib.Algebra.Order.Floor.Div
ceilDiv_le_iff_le_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [inst_4 : SMulZeroClass α β] [inst_5 : CeilDiv α β] {a : α} {b c : β},
  0 < a → (b ⌈/⌉ a ≤ c ↔ b ≤ a • c)
-- Init.Data.Nat.Basic
Nat.lt_of_le_sub_one : ∀ {m n : ℕ}, 0 < m → n ≤ m - 1 → n < m
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.inl_comp_pushoutComparison : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_2 : CategoryTheory.Limits.HasPushout f g] [inst_3 : CategoryTheory.Limits.HasPushout (G.map f) (G.map g)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (G.map f) (G.map g))
      (CategoryTheory.Limits.pushoutComparison G f g) =
    G.map (CategoryTheory.Limits.pushout.inl f g)
-- Mathlib.Order.LiminfLimsup
Filter.limsInf_le_limsInf : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {f g : Filter α},
  autoParam (Filter.IsBounded (fun x1 x2 => x1 ≥ x2) f) Filter.limsInf_le_limsInf._auto_1 →
    autoParam (Filter.IsCobounded (fun x1 x2 => x1 ≥ x2) g) Filter.limsInf_le_limsInf._auto_3 →
      (∀ (a : α), (∀ᶠ (n : α) in f, a ≤ n) → ∀ᶠ (n : α) in g, a ≤ n) → f.limsInf ≤ g.limsInf
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type w}
  [inst_1 : CategoryTheory.Limits.HasFiniteCoproducts C] (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
  {x Y : Finset (CategoryTheory.Discrete α)} (h : x ⟶ Y),
  (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj F).map h =
    CategoryTheory.Limits.Sigma.desc fun y => CategoryTheory.Limits.Sigma.ι (fun x => F.obj ↑x) ⟨↑y, ⋯⟩
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
closedBall_sub_ball : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ ε : ℝ},
  0 ≤ ε → 0 < δ → ∀ (a b : E), Metric.closedBall a ε - Metric.ball b δ = Metric.ball (a - b) (ε + δ)
-- Init.Data.UInt.Bitwise
UInt64.toUInt16_shiftLeft : ∀ (a b : UInt64), b < 16 → (a <<< b).toUInt16 = a.toUInt16 <<< b.toUInt16
-- Mathlib.Util.TransImports
/-- `#trans_imports` reports how many transitive imports the current module has.
The command takes an optional string input: `#trans_imports str` also shows the transitively
imported modules whose name begins with `str`.

Mostly for the sake of tests, the command also takes an optional `at_most x` input:
if the number of imports does not exceed `x`, then the message involves `x`, rather than the
actual, possibly varying, number of imports.
 -/
transImportsStx : Lean.ParserDescr
-- Std.Data.HashSet.Lemmas
Std.HashSet.insertMany_list_singleton : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} {k : α}, m.insertMany [k] = m.insert k
-- Mathlib.CategoryTheory.Linear.LinearFunctor
CategoryTheory.Functor.inducedFunctorLinear : ∀ (R : Type u_1) [inst : Semiring R] {C : Type u_2} {D : Type u_3} [inst_1 : CategoryTheory.Category.{v_2, u_3} D]
  [inst_2 : CategoryTheory.Preadditive D] [inst_3 : CategoryTheory.Linear R D] (F : C → D),
  CategoryTheory.Functor.Linear R (CategoryTheory.inducedFunctor F)
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Trie.node.inj : ∀ {α : Type} {values : Array α} {star : Lean.Meta.LazyDiscrTree.TrieIndex}
  {children : Std.HashMap Lean.Meta.LazyDiscrTree.Key Lean.Meta.LazyDiscrTree.TrieIndex}
  {pending : Array (Lean.Meta.LazyDiscrTree.LazyEntry α)} {values_1 : Array α}
  {star_1 : Lean.Meta.LazyDiscrTree.TrieIndex}
  {children_1 : Std.HashMap Lean.Meta.LazyDiscrTree.Key Lean.Meta.LazyDiscrTree.TrieIndex}
  {pending_1 : Array (Lean.Meta.LazyDiscrTree.LazyEntry α)},
  { values := values, star := star, children := children, pending := pending } =
      { values := values_1, star := star_1, children := children_1, pending := pending_1 } →
    values = values_1 ∧ star = star_1 ∧ children = children_1 ∧ pending = pending_1
-- Mathlib.Analysis.Fourier.ZMod
Function.Odd.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Neg α] [inst_1 : Neg β] (f : α → β), Function.Odd f = ∀ (a : α), f (-a) = -f a
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithInitial.coconeEquiv_unitIso_hom_app_hom_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Under X)} (X_1 : CategoryTheory.Limits.Cocone K),
  (CategoryTheory.WithInitial.coconeEquiv.unitIso.hom.app X_1).hom.right = CategoryTheory.CategoryStruct.id X_1.pt.right
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
/-- positive integers summing to `n`  -/
Nat.Partition.parts : {n : ℕ} → n.Partition → Multiset ℕ
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.lanCompColimIso_inv_app : ∀ {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] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F]
  [inst_4 : CategoryTheory.Limits.HasColimitsOfShape C H] [inst_5 : CategoryTheory.Limits.HasColimitsOfShape D H]
  (X : CategoryTheory.Functor C H),
  L.lanCompColimIso.inv.app X = ((L.lan.obj X).colimitIsoOfIsLeftKanExtension (L.lanUnit.app X)).inv
-- Init.Data.Array.Lemmas
Array.extract.loop.eq_def : ∀ {α : Type u_1} (as : Array α) (i j : ℕ) (bs : Array α),
  Array.extract.loop as i j bs =
    if hlt : j < as.size then
      match i with
      | 0 => bs
      | i'.succ => Array.extract.loop as i' (j + 1) (bs.push (as.getInternal j hlt))
    else bs
-- Mathlib.Geometry.Euclidean.MongePoint
/-- All triangles in an orthocentric system have the same circumradius.  -/
EuclideanGeometry.OrthocentricSystem.exists_circumradius_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : Set P},
  EuclideanGeometry.OrthocentricSystem s →
    ∃ r, ∀ (t : Affine.Triangle ℝ P), Set.range t.points ⊆ s → Affine.Simplex.circumradius t = r
-- Std.Tactic.BVDecide.LRAT.Actions
Std.Tactic.BVDecide.LRAT.Action.addEmpty : {β : Type u} → {α : Type v} → ℕ → Array ℕ → Std.Tactic.BVDecide.LRAT.Action β α
-- Mathlib.Data.Int.Bitwise
Int.bitwise.eq_1 : ∀ (f : Bool → Bool → Bool) (m n : ℕ), Int.bitwise f (Int.ofNat m) (Int.ofNat n) = Int.natBitwise f m n
-- Mathlib.Order.Grade
GradeBoundedOrder.mk : {𝕆 : Type u_5} →
  {α : Type u_6} →
    [inst : Preorder 𝕆] →
      [inst_1 : Preorder α] →
        [toGradeMinOrder : GradeMinOrder 𝕆 α] →
          (∀ ⦃a : α⦄, IsMax a → IsMax (GradeOrder.grade a)) → GradeBoundedOrder 𝕆 α
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.linear_constVAdd : ∀ (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (v : V₁), (AffineEquiv.constVAdd k P₁ v).linear = LinearEquiv.refl k V₁
-- Mathlib.Analysis.Convex.Star
starConvex_iff_openSegment_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {x : E} {s : Set E} [ZeroLEOneClass 𝕜],
  x ∈ s → (StarConvex 𝕜 x s ↔ ∀ ⦃y : E⦄, y ∈ s → openSegment 𝕜 x y ⊆ s)
-- Std.Sat.CNF.Relabel
Std.Sat.CNF.Clause.relabel_congr : ∀ {α : Type u_1} {β : Type u_2} {c : Std.Sat.CNF.Clause α} {r1 r2 : α → β},
  (∀ (v : α), Std.Sat.CNF.Clause.Mem v c → r1 v = r2 v) →
    Std.Sat.CNF.Clause.relabel r1 c = Std.Sat.CNF.Clause.relabel r2 c
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_modify : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] {k k' : α} [inst_4 : Inhabited β] {f : β → β},
  m.WF →
    Std.DHashMap.Raw.Const.get! (Std.DHashMap.Raw.Const.modify m k f) k' =
      if (k == k') = true then (Option.map f (Std.DHashMap.Raw.Const.get? m k)).get!
      else Std.DHashMap.Raw.Const.get! m k'
-- Mathlib.GroupTheory.DoubleCoset
DoubleCoset.doubleCoset_eq_image2 : ∀ {α : Type u_2} [inst : Mul α] (a : α) (s t : Set α),
  DoubleCoset.doubleCoset a s t = Set.image2 (fun x1 x2 => x1 * a * x2) s t
-- Init.Data.Float.Float
/-- Raises one floating-point number to the power of another. Typically used via the `^` operator.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`pow`.
 -/
Float.pow : Float → Float → Float
-- Mathlib.Topology.Covering.Quotient
Subgroup.isQuotientCoveringMap : ∀ {G : Type u_4} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] (S : Subgroup G),
  IsDiscrete ↑S → IsQuotientCoveringMap QuotientGroup.mk ↥S.op
-- Init.Data.SInt.Lemmas
Int8.toBitVec_toISize : ∀ (x : Int8), x.toISize.toBitVec = BitVec.signExtend System.Platform.numBits x.toBitVec
-- Mathlib.Algebra.BigOperators.Finprod
/-- **Alias** of `finprod_mem_mul_sdiff'`.

---

A more general version of `finprod_mem_mul_diff` that requires `t ∩ mulSupport f` rather than
`t` to be finite.  -/
finprod_mem_mul_diff' : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s t : Set α},
  s ⊆ t →
    (t ∩ Function.mulSupport f).Finite →
      (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t \ s), f i = ∏ᶠ (i : α) (_ : i ∈ t), f i
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.ext : ∀ {R : Type u} {inst : CommSemiring R} {M : Type u_1} {inst_1 : AddCommMonoid M} {inst_2 : Module R M} {N : Type u_2}
  {inst_3 : AddCommMonoid N} {inst_4 : Module R N} {x y : M →ₚₗ[R] N}, x.toFun' = y.toFun' → x = y
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.biInf : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : ConditionallyCompleteLinearOrderBot ι]
  [inst_1 : TopologicalSpace ι] [OrderTopology ι] [DenselyOrdered ι] [FirstCountableTopology ι] [NoMaxOrder ι]
  {κ : Type u_4} {f : MeasureTheory.Filtration ι m} {τ : κ → Ω → WithTop ι} {s : Set κ},
  s.Countable →
    ∀ [f.IsRightContinuous],
      (∀ n ∈ s, MeasureTheory.IsStoppingTime f (τ n)) → MeasureTheory.IsStoppingTime f fun ω => ⨅ n ∈ s, τ n ω
-- Mathlib.Algebra.Order.Interval.Basic
instOneInterval.eq_1 : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : One α], instOneInterval = { one := ↑1 }
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- `h.isoΩ₀` is the unique isomorphism from `h.Ω₀` to the canonical terminal object `⊤_ C`.  -/
CategoryTheory.SubobjectRepresentableBy.isoΩ₀ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      {Ω : C} →
        (h : CategoryTheory.SubobjectRepresentableBy Ω) →
          [inst_2 : CategoryTheory.Limits.HasTerminal C] → CategoryTheory.Subobject.underlying.obj h.Ω₀ ≅ ⊤_ C
-- Mathlib.RingTheory.FractionalIdeal.Extended
/-- **Alias** of `FractionalIdeal.le_one_of_extendedHom_le_one`. -/
FractionalIdeal.le_one_of_extendedHomₐ_le_one : ∀ {A : Type u_1} {K : Type u_2} (L : Type u_3) (B : Type u_4) [inst : CommRing A] [inst_1 : IsDomain A]
  [inst_2 : CommRing B] [inst_3 : IsDomain B] [inst_4 : Algebra A B] [inst_5 : Module.IsTorsionFree A B]
  [inst_6 : Field K] [inst_7 : Field L] [inst_8 : Algebra A K] [inst_9 : Algebra B L] [inst_10 : IsFractionRing A K]
  [inst_11 : IsFractionRing B L] {I : FractionalIdeal (nonZeroDivisors A) K} [inst_12 : Algebra K L]
  [inst_13 : Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsIntegral A B] [IsIntegrallyClosed A]
  [IsIntegrallyClosed B], (FractionalIdeal.extendedHom L B) I ≤ 1 → I ≤ 1
-- Mathlib.Tactic.Simproc.ExistsAndEq
/-- Generates a proof of `∃ a, p a → P'`. We assume that `fvars = [f₁, ..., fₙ]` are free variables
and `P' = ∃ f₁ ... fₙ, newBody`, and `path` leads to `a = a'` in `∃ a, p a`.

The proof follows the following structure:
```
example {α β : Type} (f : β → α) {p : α → Prop} :
    (∃ a, p a ∧ ∃ b, a = f b) → (∃ b, p (f b) ∧ f b = f b) := by
  -- withLocalDeclQ
  intro h
  refine h.elim (fun a ha ↦ ?_)
  -- withExistsElimAlongPath: following the path we unpack all existential quantifiers.
  -- at the end `hs = [hb]`.
  have h' := ha
  replace h' := h'.right
  refine Exists.elim h' (fun b hb ↦ ?_)
  replace h' := hb
  have h_eq := h'
  clear h'
  -- go: we traverse `P` and `goal` simultaneously
  have h' := ha
  refine Exists.intro b ?_
  refine And.intro ?_ ?_
  -- outside the path goal must coincide with `h_eq ▸ h'`
  · replace h' := h'.left
    exact Eq.mp (congrArg (fun t ↦ p t) h_eq) h'
  -- inside the path:
  · replace h' := h'.right
    -- when `h'` starts with existential quantifier we replace it with next hypothesis from `hs`.
    replace h' := hb
    -- at the end the goal must be `x' = x'`.
    rfl
```  -/
ExistsAndEq.mkBeforeToAfter : {u : Lean.Level} →
  {α : Q(Sort u)} →
    {p : Q(«$α» → Prop)} →
      {P' : Q(Prop)} →
        Q(«$α») → Q(Prop) → List ExistsAndEq.VarQ → ExistsAndEq.Path → Lean.MetaM Q((∃ a, «$p» a) → «$P'»)
-- Mathlib.Data.Fin.SuccPred
Fin.predAbove_castPred_of_le : ∀ {n : ℕ} (p i : Fin (n + 1)) (h : i ≤ p) (hp : p ≠ Fin.last n), (p.castPred hp).predAbove i = i.castPred ⋯
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.adjoin_eq_top_of_infinitePlace_lt : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : NumberField.RingOfIntegers K}
  {w : NumberField.InfinitePlace K},
  x ≠ 0 → (∀ ⦃w' : NumberField.InfinitePlace K⦄, w' ≠ w → w' ↑x < 1) → w.IsReal ∨ |(w.embedding ↑x).re| < 1 → ℚ[↑x] = ⊤
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
/-- Same as `IsPullback.of_iso`, but using the data and compatibilities involving
the inverse isomorphisms instead.  -/
CategoryTheory.IsPullback.of_iso' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z},
  CategoryTheory.IsPullback fst snd f g →
    ∀ {P' X' Y' Z' : C} {fst' : P' ⟶ X'} {snd' : P' ⟶ Y'} {f' : X' ⟶ Z'} {g' : Y' ⟶ Z'} (e₁ : P' ≅ P) (e₂ : X' ≅ X)
      (e₃ : Y' ≅ Y) (e₄ : Z' ≅ Z),
      CategoryTheory.CategoryStruct.comp e₁.hom fst = CategoryTheory.CategoryStruct.comp fst' e₂.hom →
        CategoryTheory.CategoryStruct.comp e₁.hom snd = CategoryTheory.CategoryStruct.comp snd' e₃.hom →
          CategoryTheory.CategoryStruct.comp e₂.hom f = CategoryTheory.CategoryStruct.comp f' e₄.hom →
            CategoryTheory.CategoryStruct.comp e₃.hom g = CategoryTheory.CategoryStruct.comp g' e₄.hom →
              CategoryTheory.IsPullback fst' snd' f' g'
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.measurable_mapNatBool : ∀ (α : Type u_1) [inst : MeasurableSpace α] [inst_1 : MeasurableSpace.CountablyGenerated α],
  Measurable (MeasurableSpace.mapNatBool α)