mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Sym.Pattern
Lean.Meta.Sym.Pattern.mk.inj : ∀ {levelParams : List Lean.Name} {varTypes : Array Lean.Expr} {varInfos? : Option Lean.Meta.Sym.ProofInstInfo}
  {pattern : Lean.Expr} {fnInfos : Lean.AssocList Lean.Name Lean.Meta.Sym.ProofInstInfo}
  {checkTypeMask? : Option (Array Bool)} {levelParams_1 : List Lean.Name} {varTypes_1 : Array Lean.Expr}
  {varInfos?_1 : Option Lean.Meta.Sym.ProofInstInfo} {pattern_1 : Lean.Expr}
  {fnInfos_1 : Lean.AssocList Lean.Name Lean.Meta.Sym.ProofInstInfo} {checkTypeMask?_1 : Option (Array Bool)},
  { levelParams := levelParams, varTypes := varTypes, varInfos? := varInfos?, pattern := pattern, fnInfos := fnInfos,
        checkTypeMask? := checkTypeMask? } =
      { levelParams := levelParams_1, varTypes := varTypes_1, varInfos? := varInfos?_1, pattern := pattern_1,
        fnInfos := fnInfos_1, checkTypeMask? := checkTypeMask?_1 } →
    levelParams = levelParams_1 ∧
      varTypes = varTypes_1 ∧
        varInfos? = varInfos?_1 ∧ pattern = pattern_1 ∧ fnInfos = fnInfos_1 ∧ checkTypeMask? = checkTypeMask?_1
-- Mathlib.Analysis.Normed.Group.NullSubmodule
isClosed_nullAddSubgroup : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M], IsClosed ↑(nullAddSubgroup M)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- If two ring homomorphisms are equal on a set, then they are equal on its subsemiring closure.  -/
RingHom.eqOn_sclosure : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {f g : R →+* S} {s : Set R},
  Set.EqOn (⇑f) (⇑g) s → Set.EqOn ⇑f ⇑g ↑(Subsemiring.closure s)
-- Init.Tactics
/-- Searches environment for definitions or theorems that can refine the goal using `apply`
with conditions resolved when possible with `solve_by_elim`.

The optional `using` clause provides identifiers in the local context that must be
used when closing the goal.

Use `+grind` to enable `grind` as a fallback discharger for subgoals.
Use `+try?` to enable `try?` as a fallback discharger for subgoals.
Use `-star` to disable fallback to star-indexed lemmas.
Use `+all` to collect all successful lemmas instead of stopping at the first.
 -/
Lean.Parser.Tactic.apply? : Lean.ParserDescr
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isSome_minKey?_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α}
  {f : β → β}, t.WF → (t.modify k f).minKey?.isSome = !t.isEmpty
-- Mathlib.Order.Category.HeytAlg
HeytAlg.coe_of : ∀ (X : Type u) [inst : HeytingAlgebra X], ↑(HeytAlg.of X) = X
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.finset_card_neighborSet_eq_degree : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {v : V} [inst : Fintype ↑(G'.neighborSet v)],
  (G'.neighborSet v).toFinset.card = G'.degree v
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.coeff_apply : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R]
  (s : HahnSeries.SummableFamily Γ R α) (g : Γ) (a : α), (s.coeff g) a = (s a).coeff g
-- Init.Data.Fin.Lemmas
Fin.add_one_pos : ∀ {n : ℕ}, ∀ i < Fin.last n, 0 < i + 1
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → ∀ (k : α), (t₁.erase k).Equiv (t₂.erase k)
-- Mathlib.Analysis.Calculus.Deriv.Add
differentiableAt_comp_neg : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {a : 𝕜}, DifferentiableAt 𝕜 (fun x => f (-x)) a ↔ DifferentiableAt 𝕜 f (-a)
-- Init.Prelude
/-- Extract the left conjunct from a conjunction. `h : a ∧ b` then
`h.left`, also notated as `h.1`, is a proof of `a`.  -/
And.left : ∀ {a b : Prop}, a ∧ b → a
-- Std.Http.Data.URI.Encoding
/-- A percent-encoded URI path segment. Valid characters are `pchar` (unreserved, sub-delims, ':', '@').
 -/
Std.Http.URI.EncodedSegment : Type
-- Std.Time.Date.Unit.Week
Std.Time.Week.instLawfulEqOrdOffset : Std.LawfulEqOrd Std.Time.Week.Offset
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
MultipliableUniformlyOn.hasProdUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {s : Set β}
  [inst_1 : UniformSpace α], MultipliableUniformlyOn f s → HasProdUniformlyOn f (fun x => ∏' (i : ι), f i x) s
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcKeepAliveParams.mk.injEq : ∀ (uri : Lean.Lsp.DocumentUri) (sessionId : UInt64) (uri_1 : Lean.Lsp.DocumentUri) (sessionId_1 : UInt64),
  ({ uri := uri, sessionId := sessionId } = { uri := uri_1, sessionId := sessionId_1 }) =
    (uri = uri_1 ∧ sessionId = sessionId_1)
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.mem_comap : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : TopologicalSpace M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : TopologicalSpace N]
  [inst_6 : Module R N] {f : M →L[R] N} {s : ClosedSubmodule R N} {x : M}, x ∈ ClosedSubmodule.comap f s ↔ f x ∈ s
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyOutgoingCall.to : Lean.Lsp.CallHierarchyOutgoingCall → Lean.Lsp.CallHierarchyItem
-- Mathlib.Topology.Category.CompHaus.Basic
/-- The category of compact Hausdorff spaces is reflective in the category of topological spaces.
 -/
compHausToTop.reflective : CategoryTheory.Reflective compHausToTop
-- Mathlib.Algebra.BigOperators.Finprod
/-- If `f a = 1` when `a ∉ s`, then the product of `f i` over `i ∈ insert a s` equals the product of
`f i` over `i ∈ s`.  -/
finprod_mem_insert_of_eq_one_if_notMem : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {a : α} {s : Set α},
  (a ∉ s → f a = 1) → ∏ᶠ (i : α) (_ : i ∈ insert a s), f i = ∏ᶠ (i : α) (_ : i ∈ s), f i
-- Init.Data.UInt.Lemmas
UInt16.toNat_div : ∀ (a b : UInt16), (a / b).toNat = a.toNat / b.toNat
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.withAuxDeclImp : {α : Type} → Lean.Name → Lean.Expr → Lean.Name → (Lean.Expr → Lean.MetaM α) → Lean.MetaM α
-- Init.Prelude
Lean.ParserDescr.brecOn.eq : ∀ {motive : Lean.ParserDescr → Sort u} (t : Lean.ParserDescr)
  (F_1 : (t : Lean.ParserDescr) → Lean.ParserDescr.below t → motive t),
  Lean.ParserDescr.brecOn t F_1 = F_1 t (Lean.ParserDescr.brecOn.go t F_1).2
-- Mathlib.GroupTheory.Coset.Basic
rightAddCosetEquivalence_rel : ∀ {α : Type u_1} [inst : Add α] (s : Set α), Equivalence (RightAddCosetEquivalence s)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.asIsoHomologyπ_inv_comp_homologyπ_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) [inst_2 : S.HasHomology] {Z : C} (h : S.homology ⟶ Z),
  CategoryTheory.CategoryStruct.comp (S.asIsoHomologyπ hf).inv (CategoryTheory.CategoryStruct.comp S.homologyπ h) = h
-- Mathlib.Computability.Partrec
Computable.list_length : ∀ {α : Type u_1} [inst : Primcodable α], Computable List.length
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageMetaData.notification.sizeOf_spec : ∀ (method : String), sizeOf (Lean.JsonRpc.MessageMetaData.notification method) = 1 + sizeOf method
-- Mathlib.Algebra.Star.Basic
InvolutiveStar.toStar : {R : Type u} → [self : InvolutiveStar R] → Star R
-- Init.Data.BitVec.Bitblast
BitVec.getLsbD_extractAndExtendBit : ∀ {w k len i : ℕ} {x : BitVec w},
  (BitVec.extractAndExtendBit k len x).getLsbD i = (decide (i = 0) && decide (0 < len) && x.getLsbD k)
-- Mathlib.ModelTheory.Semantics
/-- A special case of `realize_restrictVar`, included because we can add the `simp` attribute
to it  -/
FirstOrder.Language.Term.realize_restrictVar' : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} [inst_1 : DecidableEq α] {t : L.Term α}
  {s : Set α} (h : ↑t.varFinset ⊆ s) {v : α → M},
  FirstOrder.Language.Term.realize (v ∘ Subtype.val) (t.restrictVar (Set.inclusion h)) =
    FirstOrder.Language.Term.realize v t
-- Mathlib.Data.Option.NAry
/-- If `b` is a right identity for a binary operation `f`, then `some b` is a right identity for
`Option.map₂ f`.  -/
Option.map₂_right_identity : ∀ {α : Type u_1} {β : Type u_2} {f : α → β → α} {b : β},
  (∀ (a : α), f a b = a) → ∀ (o : Option α), Option.map₂ f o (some b) = o
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.WhiskerRight.brecOn.eq : ∀ {motive : Mathlib.Tactic.BicategoryLike.WhiskerRight → Sort u} (t : Mathlib.Tactic.BicategoryLike.WhiskerRight)
  (F_1 :
    (t : Mathlib.Tactic.BicategoryLike.WhiskerRight) → Mathlib.Tactic.BicategoryLike.WhiskerRight.below t → motive t),
  Mathlib.Tactic.BicategoryLike.WhiskerRight.brecOn t F_1 =
    F_1 t (Mathlib.Tactic.BicategoryLike.WhiskerRight.brecOn.go t F_1).2
-- Mathlib.Data.Prod.TProd
List.TProd.mk.eq_1 : ∀ {ι : Type u} {α : ι → Type v}, List.TProd.mk [] = fun x => PUnit.unit
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.mk.sizeOf_spec : ∀ {X : Type u_5} {Y : Type u_6} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : SizeOf X]
  [inst_3 : SizeOf Y] (toEquiv : X ≃ Y)
  (continuous_toFun : autoParam (Continuous toEquiv.toFun) Homeomorph.continuous_toFun._autoParam)
  (continuous_invFun : autoParam (Continuous toEquiv.invFun) Homeomorph.continuous_invFun._autoParam),
  sizeOf { toEquiv := toEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun } =
    1 + sizeOf toEquiv + sizeOf continuous_toFun + sizeOf continuous_invFun
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.ι_d_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] {G A : C} {M : ModuleCat (CategoryTheory.End G)ᵐᵒᵖ}
  (g : M ⟶ ModuleCat.of (CategoryTheory.End G)ᵐᵒᵖ (G ⟶ A)) (m : ↑M) {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun x => G) m)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.d g) h) =
    CategoryTheory.CategoryStruct.comp ((ModuleCat.Hom.hom g) m) h
-- Mathlib.Analysis.InnerProductSpace.NormPow
fderiv_norm_rpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] (x : E) {p : ℝ},
  1 < p → fderiv ℝ (fun x => ‖x‖ ^ p) x = (p * ‖x‖ ^ (p - 2)) • (innerSL ℝ) x
-- Lean.Meta.Tactic.Grind.Internalize
/-- Returns `true` if we should use `funCC` for `f`-applications.
 -/
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.useFunCongrAtFn : Lean.Expr → Lean.Meta.Grind.GrindM Bool
-- Aesop.Tree.Data
Aesop.RappData.introducedMVars : {Goal MVarCluster : Type} → Aesop.RappData Goal MVarCluster → Aesop.UnorderedArraySet Lean.MVarId
-- Init.Data.List.Attach
List.attachWith_reverse : ∀ {α : Type u_1} {P : α → Prop} {xs : List α} {H : ∀ a ∈ xs.reverse, P a},
  xs.reverse.attachWith P H = (xs.attachWith P ⋯).reverse
-- Mathlib.Algebra.Module.Congruence.Defs
SMulCon.toSetoid : {S : Type u_2} → {M : Type u_3} → [inst : SMul S M] → SMulCon S M → Setoid M
-- Mathlib.Data.Set.Prod
Set.subset_pi_iff : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : Set ι} {t : (i : ι) → Set (α i)} {s' : Set ((i : ι) → α i)},
  s' ⊆ s.pi t ↔ ∀ i ∈ s, s' ⊆ (fun x => x i) ⁻¹' t i
-- Mathlib.Data.Multiset.MapFold
Multiset.Nodup.map_on : ∀ {α : Type u_1} {β : Type v} {s : Multiset α} {f : α → β},
  (∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y) → s.Nodup → (Multiset.map f s).Nodup
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
borel_eq_generateFrom_Icc : ∀ (α : Type u_5) [inst : TopologicalSpace α] [SecondCountableTopology α] [inst_2 : LinearOrder α] [OrderTopology α],
  borel α = MeasurableSpace.generateFrom {S | ∃ l u, l ≤ u ∧ Set.Icc l u = S}
-- Mathlib.Data.List.OfFn
/-- Lists are equivalent to the sigma type of tuples of a given length.  -/
List.equivSigmaTuple : {α : Type u} → List α ≃ (n : ℕ) × (Fin n → α)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.mkIso'_hom_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H : C} (e : G ≅ H) [inst_2 : CategoryTheory.GrpObj G] [inst_3 : CategoryTheory.GrpObj H]
  [inst_4 : CategoryTheory.IsMonHom e.hom], (CategoryTheory.Grp.mkIso' e).hom.hom.hom = e.hom
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono_attachCells_cofan₂ : ∀ {X Y : SSet} (i : X ⟶ Y) [inst : CategoryTheory.Mono i] (d : ℕ) (x : ¬IsMax d),
  ((SSet.relativeCellComplexOfMono i).attachCells d x).cofan₂ =
    CategoryTheory.Limits.Cofan.mk (∐ fun i => SSet.stdSimplex.obj { len := d })
      (CategoryTheory.Limits.Sigma.ι fun i => SSet.stdSimplex.obj { len := d })
-- Mathlib.Order.Monotone.Defs
Monotone.comp : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
  {f : α → β}, Monotone g → Monotone f → Monotone (g ∘ f)
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.prod_comm : ∀ {α : Type u_1} {β : Type u_7} {M : Type u_8} {M' : Type u_9} {N : Type u_10} [inst : Zero M] [inst_1 : Zero M']
  [inst_2 : CommMonoid N] (f : α →₀ M) (g : β →₀ M') (h : α → M → β → M' → N),
  (f.prod fun x v => g.prod fun x' v' => h x v x' v') = g.prod fun x' v' => f.prod fun x v => h x v x' v'
-- Mathlib.RepresentationTheory.Induced
Representation.ind_apply : ∀ {k : Type u_1} {G : Type u_2} {H : Type u_3} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] (φ : G →* H)
  {A : Type u_4} [inst_3 : AddCommGroup A] [inst_4 : Module k A] (ρ : Representation k G A) (h : H),
  (Representation.ind φ ρ) h =
    Representation.Coinvariants.map (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) ρ)
      (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) ρ)
      { toLinearMap := LinearMap.rTensor A (MonoidAlgebra.mapDomainLinearMap k k fun x => x * h⁻¹),
        isIntertwining' := ⋯ }
-- Mathlib.Order.Lattice
left_eq_inf : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α}, a = a ⊓ b ↔ a ≤ b
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.isRelational_constantsOn : ∀ {α : Type u'} [_ie : IsEmpty α], (FirstOrder.Language.constantsOn α).IsRelational
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.self_trans_symm : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (e : M ≃+ N), e.trans e.symm = AddEquiv.refl M
-- Mathlib.CategoryTheory.Preadditive.Mat
/-- The identity matrix consists of identity morphisms on the diagonal, and zeros elsewhere.  -/
CategoryTheory.Mat_.Hom.id : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → [CategoryTheory.Preadditive C] → (M : CategoryTheory.Mat_ C) → M.Hom M
-- Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
SimpleGraph.binomialRandom_singleton : ∀ {V : Type u_1} (p : ↑unitInterval) [Finite V] (G : SimpleGraph V),
  (SimpleGraph.binomialRandom V p) {G} =
    ↑(unitInterval.toNNReal p) ^ G.edgeSet.ncard *
      ↑(unitInterval.toNNReal (unitInterval.symm p)) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)
-- Mathlib.FieldTheory.PolynomialGaloisGroup
/-- The function taking `rootSet p p.SplittingField` to `rootSet p E`. This is actually a bijection,
see `Polynomial.Gal.mapRoots_bijective`.  -/
Polynomial.Gal.mapRoots : {F : Type u_1} →
  [inst : Field F] →
    (p : Polynomial F) →
      (E : Type u_2) →
        [inst_1 : Field E] →
          [inst_2 : Algebra F E] →
            [Fact (Polynomial.map (algebraMap F E) p).Splits] → ↑(p.rootSet p.SplittingField) → ↑(p.rootSet E)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.contains_of_contains_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : (a : α) → β a → Bool} {k : α},
  (Std.ExtDHashMap.filter f m).contains k = true → m.contains k = true
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.Hom.ext_iff : ∀ {A B : AddCommGrpCat} {x y : A.Hom B}, x = y ↔ x.hom' = y.hom'
-- Mathlib.Algebra.Order.CompleteField
ConditionallyCompleteLinearOrderedField.inducedMap_add : ∀ (α : Type u_2) (β : Type u_3) [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : Field β]
  [inst_4 : ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] (x y : α),
  ConditionallyCompleteLinearOrderedField.inducedMap α β (x + y) =
    ConditionallyCompleteLinearOrderedField.inducedMap α β x + ConditionallyCompleteLinearOrderedField.inducedMap α β y
-- Mathlib.Combinatorics.Quiver.Covering
Prefunctor.star_snd : ∀ {U : Type u_1} [inst : Quiver U] {V : Type u_2} [inst_1 : Quiver V] (φ : U ⥤q V) (u : U) (a : Quiver.Star u),
  (φ.star u a).snd = φ.map a.snd
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
/-- A projective object admits a trivial projective resolution: itself in degree 0.  -/
CategoryTheory.ProjectiveResolution.self : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (Z : C) → [CategoryTheory.Projective Z] → CategoryTheory.ProjectiveResolution Z
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k k' : α}
  {f : Option β → Option β},
  (t.alter k f).contains k' = if cmp k k' = Ordering.eq then (f t[k]?).isSome else t.contains k'
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
instMulSemiringActionSubtypeMemSubalgebraIntegralClosure : {G : Type u_1} →
  {R : Type u_2} →
    {K : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing K] →
          [inst_2 : Algebra R K] →
            [inst_3 : Group G] →
              [inst_4 : MulSemiringAction G K] → [SMulCommClass G R K] → MulSemiringAction G ↥(integralClosure R K)
-- Std.Sync.RecursiveMutex
_private.Std.Sync.RecursiveMutex.0.Std.RecursiveMutex.mk : {α : Type} → IO.Ref α → Std.BaseRecursiveMutex → Std.RecursiveMutex α
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.hom_stalk_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [instCC : CategoryTheory.ConcreteCategory C FC]
  [inst_2 : CategoryTheory.Limits.HasColimits C] [CategoryTheory.Limits.HasLimits C]
  [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)]
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)]
  [(CategoryTheory.forget C).ReflectsIsomorphisms] {X Y : AlgebraicGeometry.SheafedSpace C} (f g : X ⟶ Y)
  (h : f.hom.base = g.hom.base),
  (∀ (x : ↑↑X.toPresheafedSpace),
      AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f.hom x =
        CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkCongr ⋯).hom
          (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap g.hom x)) →
    f = g
-- Mathlib.Geometry.Convex.Cone.Pointed
/-- Coercion from submodules to pointed cones as an order embedding.  -/
PointedCone.ofSubmoduleEmbedding : {R : Type u_1} →
  {E : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] →
        [inst_2 : IsOrderedRing R] →
          [inst_3 : AddCommMonoid E] → [inst_4 : Module R E] → Submodule R E ↪o PointedCone R E
-- Mathlib.Computability.TuringMachine.Computable
Turing.FinTM2.mk.injEq : ∀ {K : Type} [kDecidableEq : DecidableEq K] [kFin : Fintype K] (k₀ k₁ : K) (Γ : K → Type) (Λ : Type) (main : Λ)
  [ΛFin : Fintype Λ] (σ : Type) (initialState : σ) [σFin : Fintype σ] [Γk₀Fin : Fintype (Γ k₀)]
  (m : Λ → Turing.TM2.Stmt Γ Λ σ) (K_1 : Type) (kDecidableEq_1 : DecidableEq K_1) (kFin_1 : Fintype K_1)
  (k₀_1 k₁_1 : K_1) (Γ_1 : K_1 → Type) (Λ_1 : Type) (main_1 : Λ_1) (ΛFin_1 : Fintype Λ_1) (σ_1 : Type)
  (initialState_1 : σ_1) (σFin_1 : Fintype σ_1) (Γk₀Fin_1 : Fintype (Γ_1 k₀_1))
  (m_1 : Λ_1 → Turing.TM2.Stmt Γ_1 Λ_1 σ_1),
  ({ K := K, kDecidableEq := kDecidableEq, kFin := kFin, k₀ := k₀, k₁ := k₁, Γ := Γ, Λ := Λ, main := main, ΛFin := ΛFin,
        σ := σ, initialState := initialState, σFin := σFin, Γk₀Fin := Γk₀Fin, m := m } =
      { K := K_1, kDecidableEq := kDecidableEq_1, kFin := kFin_1, k₀ := k₀_1, k₁ := k₁_1, Γ := Γ_1, Λ := Λ_1,
        main := main_1, ΛFin := ΛFin_1, σ := σ_1, initialState := initialState_1, σFin := σFin_1, Γk₀Fin := Γk₀Fin_1,
        m := m_1 }) =
    (K = K_1 ∧
      kDecidableEq ≍ kDecidableEq_1 ∧
        kFin ≍ kFin_1 ∧
          k₀ ≍ k₀_1 ∧
            k₁ ≍ k₁_1 ∧
              Γ ≍ Γ_1 ∧
                Λ = Λ_1 ∧
                  main ≍ main_1 ∧
                    ΛFin ≍ ΛFin_1 ∧
                      σ = σ_1 ∧ initialState ≍ initialState_1 ∧ σFin ≍ σFin_1 ∧ Γk₀Fin ≍ Γk₀Fin_1 ∧ m ≍ m_1)
-- Mathlib.Order.Filter.NAry
/-- Symmetric statement to `Filter.map_map₂_right_anticomm`.  -/
Filter.map_map₂_antidistrib_right : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {m : α → β → γ} {f : Filter α}
  {g : Filter β} {n : γ → δ} {m' : β → α' → δ} {n' : α → α'},
  (∀ (a : α) (b : β), n (m a b) = m' b (n' a)) → Filter.map n (Filter.map₂ m f g) = Filter.map₂ m' g (Filter.map n' f)
-- ProofWidgets.Component.OfRpcMethod
ProofWidgets.ofRpcMethodTemplate : String
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedLinearMap.continuous : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F] {f : E → F},
  IsBoundedLinearMap 𝕜 f → Continuous f
-- Mathlib.Algebra.Category.AlgCat.Limits
AlgCat.forget₂Module_preservesLimits : ∀ {R : Type u} [inst : CommRing R],
  CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ (AlgCat R) (ModuleCat R))
-- Mathlib.LinearAlgebra.Dimension.Basic
/-- Note: if the rank of a module is infinite, it may not contain a linear independent subset
with cardinality equal to the rank, see
https://mathoverflow.net/questions/263020/maximum-cardinal-of-a-set-of-linearly-independent-vectors-in-a-module.  -/
Module.le_rank_iff_exists_finset : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial R] {n : ℕ},
  ↑n ≤ Module.rank R M ↔ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s
-- Mathlib.Logic.Equiv.Defs
/-- Transporting a sigma type through an equivalence of the base and a family of equivalences
of matching fibers  -/
Equiv.sigmaCongr : {α₁ : Type u_1} →
  {α₂ : Type u_2} →
    {β₁ : α₁ → Type u_3} → {β₂ : α₂ → Type u_4} → (f : α₁ ≃ α₂) → ((a : α₁) → β₁ a ≃ β₂ (f a)) → Sigma β₁ ≃ Sigma β₂
-- Mathlib.Analysis.RCLike.Basic
RCLike.mul_im_I_ax : ∀ {K : semiOutParam (Type u_1)} [self : RCLike K] (z : K), RCLike.im z * RCLike.im RCLike.I = RCLike.im z
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Array
Array.toListRev_iterFromIdxM : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} [LawfulMonad m] {array : Array β} {pos : ℕ},
  (array.iterFromIdxM m pos).toListRev = pure (List.drop pos array.toList).reverse
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.liftActionCore : Lean.Meta.Grind.Action → Lean.Elab.Tactic.Grind.GrindTacticM Lean.Elab.Tactic.Grind.LiftActionCoreResult
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Power.denote.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (k : ℕ) → motive k),
  (match 0 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | k => h_3 k) =
    h_1 ()
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsMaximumIndepSet.congr_simp : ∀ {α : Type u_3} [inst : Finite α] (G G_1 : SimpleGraph α),
  G = G_1 → ∀ (s s_1 : Finset α), s = s_1 → G.IsMaximumIndepSet s = G_1.IsMaximumIndepSet s_1
-- Init.System.ST
/-- References  -/
ST.RefPointed : NonemptyType
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_diff_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₁ \ m₂ ↔ k ∈ m₁ ∧ k ∉ m₂
-- Mathlib.Order.Filter.Map
Filter.sInter_comap_sets : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (F : Filter β), ⋂₀ (Filter.comap f F).sets = ⋂ U ∈ F, f ⁻¹' U