mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.induce_mono : ∀ {V : Type u} {G : SimpleGraph V} {G' G'' : G.Subgraph} {s s' : Set V}, G' ≤ G'' → s ⊆ s' → G'.induce s ≤ G''.induce s'
-- Init.Data.String.Lemmas.Pattern.Split.Basic
String.Slice.Pattern.Model.split_eq_of_not_matchesAt : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.Model.StrictPatternModel pat] {s : String.Slice} {firstRejected start : s.Pos}
  (stop : s.Pos) (h₀ : start ≤ stop) {hle : firstRejected ≤ start},
  (∀ (p : s.Pos), start ≤ p → p < stop → ¬String.Slice.Pattern.Model.MatchesAt pat p) →
    String.Slice.Pattern.Model.split pat firstRejected start hle =
      String.Slice.Pattern.Model.split pat firstRejected stop ⋯
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.support_coeff_C_mul_T_of_ne_zero : ∀ {R : Type u_1} [inst : Semiring R] {a : R},
  a ≠ 0 → ∀ (n : ℤ), (LaurentPolynomial.C a * LaurentPolynomial.T n).coeff.support = {n}
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.RightExtension.w : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  {s t : CategoryTheory.Bicategory.RightExtension f g} (η : s ⟶ t),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f η.left) t.counit = s.counit
-- Batteries.Data.Nat.Lemmas
Nat.mul_add_lt_mul_of_lt_of_lt : ∀ {m n x y : ℕ}, x < m → y < n → n * x + y < m * n
-- Mathlib.CategoryTheory.Comma.Arrow
/-- The left part of a morphism in the category of arrows.  -/
CategoryTheory.Arrow.Hom.left : {T : Type u} → [inst : CategoryTheory.Category.{v, u} T] → {X Y : CategoryTheory.Arrow T} → (X ⟶ Y) → (X.left ⟶ Y.left)
-- Std.Data.ExtHashSet.Basic
/-- Creates a new empty hash set. The optional parameter `capacity` can be supplied to presize the
set so that it can hold the given number of elements without reallocating. It is also possible to
use the empty collection notations `∅` and `{}` to create an empty hash set with the default
capacity.
 -/
Std.ExtHashSet.emptyWithCapacity : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → optParam ℕ 8 → Std.ExtHashSet α
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.skeleton_top : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D],
  ↑(Topology.RelCWComplex.skeleton C ⊤) = C
-- Mathlib.Order.Monotone.Monovary
Monotone.antivary : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
  [inst_2 : LinearOrder ι], Monotone f → Antitone g → Antivary f g
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.baseChange_lmul : ∀ {R : Type u_1} {B : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring B] [inst_2 : Algebra R B] {A : Type u_3}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] (f : B),
  LinearMap.baseChange A ((Algebra.lmul R B) f) = (Algebra.lmul A (TensorProduct R A B)) (1 ⊗ₜ[R] f)
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Std.DHashMap.Internal.Raw₀.Const.insertMany.eq_1 : ∀ {α : Type u} {β : Type v} {ρ : Type w} [inst : ForIn Id ρ (α × β)] [inst_1 : BEq α] [inst_2 : Hashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (l : ρ),
  Std.DHashMap.Internal.Raw₀.Const.insertMany m l =
    (have r := ⟨m, ⋯⟩;
      do
      let __s ←
        forIn l r fun x __s =>
            let r := __s;
            match x with
            | (a, b) =>
              have r := ⟨(↑r).insert a b, ⋯⟩;
              pure (ForInStep.yield r)
      have r :
        { m' //
          ∀ (P : (Std.DHashMap.Internal.Raw₀ α fun x => β) → Prop),
            (∀ {m'' : Std.DHashMap.Internal.Raw₀ α fun x => β} {a : α} {b : β}, P m'' → P (m''.insert a b)) →
              P m → P m' } :=
        __s
      pure r).run
-- Lean.Meta.SizeOf
_private.Lean.Meta.SizeOf.0.Lean.Meta.SizeOfSpecNested.main.step : Lean.Expr → Lean.Expr → Lean.Meta.SizeOfSpecNested.M Lean.Expr
-- Mathlib.CategoryTheory.Localization.Opposite
CategoryTheory.Functor.IsLocalization.unop : ∀ {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ᵒᵖ)
  (W : CategoryTheory.MorphismProperty Cᵒᵖ) [L.IsLocalization W], L.unop.IsLocalization W.unop
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.Catch : Type
-- Init.Data.List.Sublist
List.nil_subset : ∀ {α : Type u_1} (l : List α), [] ⊆ l
-- Mathlib.MeasureTheory.Integral.CircleIntegral
CircleIntegrable.neg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℂ → E} {c : ℂ} {R : ℝ},
  CircleIntegrable f c R → CircleIntegrable (-f) c R
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.nnnorm_lt_iff_of_nonempty : ∀ {α : Type u_1} {E : Type u_3} [inst : TopologicalSpace α] [inst_1 : CompactSpace α]
  [inst_2 : SeminormedAddCommGroup E] (f : C(α, E)) [Nonempty α] {M : NNReal}, ‖f‖₊ < M ↔ ∀ (x : α), ‖f x‖₊ < M
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
/-- If `transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤`,
then the monomorphism `f` is a transfinite composition of pushouts of
monomorphisms in the family `generatingMonomorphisms G`.  -/
CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.transfiniteCompositionOfShapeOfEqTop : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {G : C} →
      [inst_1 : CategoryTheory.Abelian C] →
        (hG : CategoryTheory.IsSeparator G) →
          {X : C} →
            [inst_2 : CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] →
              {A : C} →
                {f : A ⟶ X} →
                  [inst_3 : CategoryTheory.Mono f] →
                    {J : Type w} →
                      [inst_4 : LinearOrder J] →
                        [inst_5 : OrderBot J] →
                          [inst_6 : SuccOrder J] →
                            [inst_7 : WellFoundedLT J] →
                              {j : J} →
                                transfiniteIterate
                                      (CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject hG)
                                      j (CategoryTheory.Subobject.mk f) =
                                    ⊤ →
                                  (CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms
                                          G).pushouts.TransfiniteCompositionOfShape
                                    (↑(Set.Iic j)) f
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.interFst_s₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  (F : CategoryTheory.PreZeroHypercover S)
  [inst_1 : ∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] (i : (E.inter F).I₀),
  (E.interFst F).s₀ i = i.1
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesMap'_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData),
  CategoryTheory.ShortComplex.opcyclesMap' (CategoryTheory.CategoryStruct.id S) h h =
    CategoryTheory.CategoryStruct.id h.Q
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.mul_one : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (φ : MvPowerSeries σ R), φ * 1 = φ
-- Mathlib.Probability.Moments.IntegrableExpMul
/-- If `ω ↦ exp (t * X ω)` is integrable at `t` and `-t` for `t ≠ 0`, then `ω ↦ |X ω| ^ p` is
integrable for all nonnegative `p : ℝ`.  -/
ProbabilityTheory.integrable_rpow_abs_of_integrable_exp_mul : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ},
  t ≠ 0 →
    MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ →
      MeasureTheory.Integrable (fun ω => Real.exp (-t * X ω)) μ →
        ∀ {p : ℝ}, 0 ≤ p → MeasureTheory.Integrable (fun ω => |X ω| ^ p) μ
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
DividedPowers.CharP.dividedPowers.eq_1 : ∀ (A : Type u_1) [inst : CommRing A] (p : ℕ) [inst_1 : CharP A p] [inst_2 : Fact (Nat.Prime p)] {I : Ideal A}
  [inst_3 : DecidablePred fun x => x ∈ I] (hIp : I ^ p = 0),
  DividedPowers.CharP.dividedPowers A p hIp = DividedPowers.IsNilpotent.dividedPowers ⋯ hIp
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.length_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.keys.length = t.size
-- Mathlib.Data.List.Lattice
List.mem_union_right : ∀ {α : Type u_1} {l₂ : List α} {a : α} [inst : DecidableEq α] (l₁ : List α), a ∈ l₂ → a ∈ l₁ ∪ l₂
-- Mathlib.Algebra.Order.Kleene
IdemCommSemiring.mk : {α : Type u_5} →
  [toCommSemiring : CommSemiring α] →
    [toSemilatticeSup : SemilatticeSup α] →
      [toOrderBot : OrderBot α] →
        autoParam (∀ (a b : α), a + b = a ⊔ b) IdemSemiring.add_eq_sup._autoParam → IdemCommSemiring α
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.keyAtIdx! : {α : Type u} → {β : α → Type v} → [Inhabited α] → Std.DTreeMap.Internal.Impl α β → ℕ → α
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.closure_induction_left : ∀ {M : Type u_1} [inst : Monoid M] {s : Set M} {motive : (m : M) → m ∈ Submonoid.closure s → Prop},
  motive 1 ⋯ →
    (∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ Submonoid.closure s), motive y hy → motive (x * y) ⋯) →
      ∀ {x : M} (h : x ∈ Submonoid.closure s), motive x h
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.instAlgebraCarrierStalkCommRingCatStructurePresheafInCommRingCat : {R : Type u} →
  [inst : CommRing R] →
    (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) →
      Algebra R ↑((AlgebraicGeometry.structurePresheafInCommRingCat R).stalk x)
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
/-- This could be considered as a simp lemma, but there are many situations where it makes something
simple into something more complicated.  -/
OpenPartialHomeomorph.trans_source : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z),
  (e.trans e').source = e.source ∩ ↑e ⁻¹' e'.source
-- Aesop.Tree.ExtractScript
Aesop.ExtractScript.recordStep : Aesop.Script.Step → Aesop.ExtractScriptM Unit
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron'.comm₄_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : Z₁₂ ⟶ X₁}
  {w₁₂ : X₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₂}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₂₃}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₃}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (self : CategoryTheory.Triangulated.Octahedron' comm h₁₂ h₂₃ h₁₃) {Z : C} (h : X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.m₃ (CategoryTheory.CategoryStruct.comp v₂₃ h) =
    CategoryTheory.CategoryStruct.comp v₁₃ (CategoryTheory.CategoryStruct.comp u₁₂ h)
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
Submodule.coe_mulMap_comp_eq : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (M N : Submodule R S)
  {T : Type w} [inst_3 : Semiring T] [inst_4 : Algebra R T] (f : S →ₐ[R] T),
  ⇑((Submodule.map (↑f) M).mulMap (Submodule.map (↑f) N)) ∘
      ⇑(TensorProduct.map ((↑f).submoduleMap M) ((↑f).submoduleMap N)) =
    ⇑f ∘ ⇑(M.mulMap N)
-- Mathlib.Data.Int.GCD
_private.Mathlib.Data.Int.GCD.0.Nat.xgcdAux_P : ∀ (x y : ℕ) {r r' : ℕ} {s t s' t' : ℤ},
  Nat.P✝ x y (r, s, t) → Nat.P✝ x y (r', s', t') → Nat.P✝ x y (r.xgcdAux s t r' s' t')
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.CoreMonoidal.μIso_hom_natural_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} (self : F.CoreMonoidal) {X Y : C} (f : X ⟶ Y) (X' : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X'))
      (self.μIso Y X').hom =
    CategoryTheory.CategoryStruct.comp (self.μIso X X').hom
      (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X'))
-- Lean.Meta.Tactic.Grind.PP
_private.Lean.Meta.Tactic.Grind.PP.0.Lean.Meta.Grind.instInhabitedResult : Inhabited Lean.Meta.Grind.Result✝
-- Mathlib.Order.UpperLower.Closure
IsLowerSet.disjoint_upperClosure_left : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α}, IsLowerSet t → (Disjoint (↑(upperClosure s)) t ↔ Disjoint s t)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.lift_fst_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  (α : M ⟶ K) (β : CochainComplex.HomComplex.Cochain M L (-1))
  (hαβ :
    CochainComplex.HomComplex.δ (-1) 0 β +
        CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp α φ) =
      0)
  {Z : CochainComplex C ℤ} (h : K ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCocone.lift φ α β hαβ)
      (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCocone.fst φ) h) =
    CategoryTheory.CategoryStruct.comp α h
-- Mathlib.Topology.Maps.OpenQuotient
IsOpenQuotientMap.of_comp_iff : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y} {g : Y → Z},
  IsOpenQuotientMap f → (IsOpenQuotientMap (g ∘ f) ↔ IsOpenQuotientMap g)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.sum_monomial_index : ∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : AddCommMonoid S] {n : ℕ} (a : R) (f : ℕ → R → S),
  f n 0 = 0 → ((Polynomial.monomial n) a).sum f = f n a
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.getLast!.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match [] with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_1 ()
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (s : Finset β) (f : β → α),
  s.sup f = Finset.fold (fun x1 x2 => x1 ⊔ x2) ⊥ f s
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Gauss
/-- Implementation of `getTableau` in `GaussM` monad.  -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.Gauss.getTableauImp : {n m : ℕ} →
  {matType : ℕ → ℕ → Type} →
    [inst : Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] →
      Mathlib.Tactic.Linarith.SimplexAlgorithm.Gauss.GaussM n m matType
        (Mathlib.Tactic.Linarith.SimplexAlgorithm.Tableau matType)
-- Lean.Meta.Tactic.Grind.EMatch
/-- Helper function for `applyAssignment.  -/
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.processUnassigned : (mvars : Array Lean.Expr) →
  (i : ℕ) → Lean.Expr → i < mvars.size → OptionT (StateT Lean.Meta.Grind.EMatch.Choice Lean.Meta.Grind.EMatch.M) Unit
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.preimage : ∀ {α : Type u} {β : Type v} {l : Filter α} {f g : α → β}, f =ᶠ[l] g → ∀ (s : Set β), f ⁻¹' s =ᶠ[l] g ⁻¹' s
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isIntegral_of_isClosedMap_comap_mapRingHom : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  IsClosedMap (PrimeSpectrum.comap (Polynomial.mapRingHom f)) → f.IsIntegral
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.preΨ_neg : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R) (n : ℤ), W.preΨ (-n) = -W.preΨ n
-- Init.Data.UInt.Bitwise
instLawfulCommIdentityUInt16HAndNegOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 &&& x2) (-1)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_diff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α],
  m₁.WF → m₂.WF → ∀ {k : α}, (m₁ \ m₂).getKey! k = if k ∈ m₂ then default else m₁.getKey! k
-- Mathlib.Data.Finset.Defs
Finset.decidableEq : {α : Type u_1} → [DecidableEq α] → DecidableEq (Finset α)
-- Mathlib.Analysis.InnerProductSpace.Calculus
contDiffOn_euclidean : ∀ {𝕜 : Type u_1} {ι : Type u_2} {H : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup H]
  [inst_2 : NormedSpace 𝕜 H] {f : H → EuclideanSpace 𝕜 ι} {t : Set H} [inst_3 : Fintype ι] {n : WithTop ℕ∞},
  ContDiffOn 𝕜 n f t ↔ ∀ (i : ι), ContDiffOn 𝕜 n (fun x => (f x).ofLp i) t
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableDiv.mk : ∀ {G₀ : Type u_2} [inst : MeasurableSpace G₀] [inst_1 : Div G₀],
  autoParam (∀ (c : G₀), Measurable fun x => c / x) MeasurableDiv.measurable_const_div._autoParam →
    autoParam (∀ (c : G₀), Measurable fun x => x / c) MeasurableDiv.measurable_div_const._autoParam → MeasurableDiv G₀
-- Mathlib.Topology.Separation.Hausdorff
/-- A continuous injective map from a compact space to a Hausdorff space is a closed embedding.  -/
Continuous.isClosedEmbedding : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [CompactSpace X] [T2Space Y]
  {f : X → Y}, Continuous f → Function.Injective f → Topology.IsClosedEmbedding f
-- Mathlib.Algebra.Lie.Basic
instLieModuleInt : ∀ {L : Type v} {M : Type w} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M], LieModule ℤ L M
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey!_le_maxKey!_insertIfNew! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF →
    t.isEmpty = false →
      ∀ {k : α} {v : β k}, (compare t.maxKey! (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).maxKey!).isLE = true
-- Lean.Environment
_private.Lean.Environment.0.Lean.finalizeImport.unsafe_5 : Lean.Environment → BaseIO Lean.Environment
-- Mathlib.RingTheory.Localization.AtPrime.Extension
/-- The isomorphism `S ⧸ P ≃+* Sₚ ⧸ P·Sₚ`, where `Sₚ` is the localization of `S` at the (image) of
the complement of `p` and `P` is a maximal ideal of `S` above `p`.
Note that this isomorphism makes the obvious diagram involving `R ⧸ p ≃+* Rₚ ⧸ maximalIdeal Rₚ`
commute, see `IsLocalization.AtPrime.algebraMap_equivQuotMaximalIdeal_symm_apply`.
 -/
IsLocalization.AtPrime.equivQuotientMapOfIsMaximal : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (p : Ideal R) →
            [inst_3 : p.IsPrime] →
              (Sₚ : Type u_4) →
                [inst_4 : CommRing Sₚ] →
                  [inst_5 : Algebra S Sₚ] →
                    [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] →
                      (P : Ideal S) →
                        [hPp : P.LiesOver p] → [P.IsMaximal] → S ⧸ P ≃+* Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P
-- Batteries.Classes.Order
Std.LawfulCmp.toLawfulEqCmp : ∀ {α : Type u_1} {inst : LE α} {inst_1 : LT α} {cmp : α → α → Ordering} [self : Std.LawfulCmp cmp], Std.LawfulEqCmp cmp
-- Mathlib.Logic.Unique
eq_const_of_subsingleton : ∀ {α : Sort u_1} {β : Sort u_2} [Subsingleton α] (f : α → β) (a : α), f = Function.const α (f a)
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.instHasLeftCalculusOfFractionsTrWOfIsTriangulatedOfIsTriangulated : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [CategoryTheory.IsTriangulated C] [P.IsTriangulated],
  P.trW.HasLeftCalculusOfFractions
-- Mathlib.Combinatorics.Additive.Corner.Defs
isCornerFree_image : ∀ {G : Type u_1} {H : Type u_2} [inst : AddCommMonoid G] [inst_1 : AddCommMonoid H] {A : Set (G × G)} {s : Set G}
  {t : Set H} {f : G → H}, IsAddFreimanIso 2 s t f → A ⊆ s ×ˢ s → (IsCornerFree (Prod.map f f '' A) ↔ IsCornerFree A)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.entryAtIdx.match_1.congr_eq_1 : ∀ {α : Type u_1} {β : Type u_2}
  (motive : (x : Std.DTreeMap.Internal.Impl α fun x => β) → x.Balanced → (x_2 : ℕ) → x_2 < x.size → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl α fun x => β) (x_1 : x.Balanced) (x_2 : ℕ) (x_3 : x_2 < x.size)
  (h_1 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l' r' : Std.DTreeMap.Internal.Impl α fun x => β) →
            (hl : (Std.DTreeMap.Internal.Impl.inner size k v l' r').Balanced) →
              (n : ℕ) →
                (h : n < (Std.DTreeMap.Internal.Impl.inner size k v l' r').size) →
                  motive (Std.DTreeMap.Internal.Impl.inner size k v l' r') hl n h)
  (size : ℕ) (k : α) (v : β) (l' r' : Std.DTreeMap.Internal.Impl α fun x => β)
  (hl : (Std.DTreeMap.Internal.Impl.inner size k v l' r').Balanced) (n : ℕ)
  (h : n < (Std.DTreeMap.Internal.Impl.inner size k v l' r').size),
  x = Std.DTreeMap.Internal.Impl.inner size k v l' r' →
    x_1 ≍ hl →
      x_2 = n →
        x_3 ≍ h →
          (match x, x_1, x_2, x_3 with
            | Std.DTreeMap.Internal.Impl.inner size k v l' r', hl, n, h => h_1 size k v l' r' hl n h) ≍
            h_1 size k v l' r' hl n h
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_filterMap_le_size : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w} [EquivBEq α]
  [LawfulHashable α] {f : (a : α) → β a → Option (γ a)}, (Std.DHashMap.filterMap f m).size ≤ m.size
-- Mathlib.RingTheory.WittVector.Truncated
/-- `truncate n` is a ring homomorphism that truncates `x` to its first `n` entries
to obtain a `TruncatedWittVector`, which has the same base `p` as `x`.  -/
WittVector.truncate : {p : ℕ} →
  (n : ℕ) →
    {R : Type u_1} → [inst : CommRing R] → [inst_1 : Fact (Nat.Prime p)] → WittVector p R →+* TruncatedWittVector p n R
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.homologyMap'_nullHomotopic : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (H₁ : S₁.HomologyData) (H₂ : S₂.HomologyData) (h₀ : S₁.X₁ ⟶ S₂.X₁)
  (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃)
  (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0),
  CategoryTheory.ShortComplex.homologyMap' (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁ H₂ = 0
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
IsIntegralClosure.of_isIntegralClosure_of_isIntegrallyClosedIn : ∀ (R : Type u_4) (S : Type u_5) (T : Type u_6) (U : Type u_7) [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : CommRing T] [inst_3 : CommRing U] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : Algebra R U]
  [inst_7 : Algebra S U] [inst_8 : Algebra T U] [IsScalarTower S T U] [IsScalarTower R T U] [IsIntegralClosure S R T]
  [IsIntegrallyClosedIn T U], IsIntegralClosure S R U
-- Mathlib.Algebra.Ring.Ext
NonAssocSemiring.ext_iff : ∀ {R : Type u} {inst₁ inst₂ : NonAssocSemiring R}, inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul