mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.WithBot
WithTop.coe_sup : ∀ {α : Type u_1} [inst : SemilatticeSup α] (a b : α), ↑(a ⊔ b) = ↑a ⊔ ↑b
-- Mathlib.CategoryTheory.Elements
CategoryTheory.groupoidOfElements : {G : Type u} →
  [inst : CategoryTheory.Groupoid G] → (F : CategoryTheory.Functor G (Type w)) → CategoryTheory.Groupoid F.Elements
-- Mathlib.Topology.Instances.Matrix
instContinuousAddMatrix : ∀ {m : Type u_4} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace R] [inst_1 : Add R] [ContinuousAdd R],
  ContinuousAdd (Matrix m n R)
-- Mathlib.Algebra.Vertex.HVertexOperator
HVertexOperator.ext_iff : ∀ {Γ : Type u_1} [inst : PartialOrder Γ] {R : Type u_2} {V : Type u_3} {W : Type u_4} [inst_1 : CommRing R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : AddCommGroup W] [inst_5 : Module R W]
  {A B : HVertexOperator Γ R V W}, A = B ↔ ∀ (v : V), A v = B v
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
/-- A `2`-simplex with prescribed `1`-dimensional faces  -/
SSet.Truncated.Edge.CompStruct.simplex : {X : SSet.Truncated 2} →
  {x₀ x₁ x₂ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })} →
    {e₀₁ : SSet.Truncated.Edge x₀ x₁} →
      {e₁₂ : SSet.Truncated.Edge x₁ x₂} →
        {e₀₂ : SSet.Truncated.Edge x₀ x₂} →
          e₀₁.CompStruct e₁₂ e₀₂ →
            X.obj (Opposite.op { obj := { len := 2 }, property := SSet.Truncated.Edge.CompStruct._proof_1 })
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousLinearMap.flipLinear_flipMultilinear : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : SeminormedAddCommGroup G']
  [inst_6 : NormedSpace 𝕜 G'] [inst_7 : Fintype ι] (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'),
  f.flipMultilinear.flipLinear = f
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
nndist_ofMul : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] (a b : X), nndist (Additive.ofMul a) (Additive.ofMul b) = nndist a b
-- Mathlib.Tactic.DeriveCountable
/-- Specialized step of the injectivity argument, pops the head of the pairs and decodes.
 -/
Mathlib.Deriving.Countable.pair_encode_step : ∀ {p : Prop} {α : Sort u_1} [inst : Countable α] {a b : α} {m n : ℕ},
  (a = b → m = n → p) →
    Nat.pair (Mathlib.Deriving.Countable.encode a) m = Nat.pair (Mathlib.Deriving.Countable.encode b) n → p
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.sum_lt_sum_of_ne_nil : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [AddLeftStrictMono M] [AddLeftMono M]
  [AddRightStrictMono M] [AddRightMono M] {l : List ι},
  l ≠ [] → ∀ (f g : ι → M), (∀ i ∈ l, f i < g i) → (List.map f l).sum < (List.map g l).sum
-- Lean.Elab.Binders
_private.Lean.Elab.Binders.0.Lean.Elab.Term.elabBinderViews.loop : {α : Type} →
  Array Lean.Elab.Term.BinderView →
    (Array (Lean.Syntax × Lean.Expr) → Lean.Elab.TermElabM α) →
      ℕ → Array (Lean.Syntax × Lean.Expr) → Lean.Elab.TermElabM α
-- Mathlib.Probability.ProductMeasure
/-- Restricting the product measure to a product indexed by a finset yields the usual
product measure.  -/
MeasureTheory.Measure.infinitePi_map_restrict : ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → MeasureTheory.Measure (X i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {I : Finset ι},
  MeasureTheory.Measure.map I.restrict (MeasureTheory.Measure.infinitePi μ) = MeasureTheory.Measure.pi fun i => μ ↑i
-- Mathlib.Lean.Meta
_private.Mathlib.Lean.Meta.0.Lean.Elab.Tactic.TacticM.runCore : {α : Type} →
  Lean.Elab.Tactic.TacticM α →
    Lean.Elab.Tactic.Context → Lean.Elab.Tactic.State → Lean.Elab.TermElabM (α × Lean.Elab.Tactic.State)
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.unit_comp_map_eq_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {A : C} {B : D} (f : F.obj A ⟶ B)
  (g : A ⟶ G.obj B),
  CategoryTheory.CategoryStruct.comp (adj.unit.app A) (G.map f) = g ↔
    f = CategoryTheory.CategoryStruct.comp (F.map g) (adj.counit.app B)
-- Init.Data.Int.DivMod.Basic
Int.ofNat_fdiv : ∀ (m n : ℕ), ↑(m / n) = (↑m).fdiv ↑n
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.instIsScalarTowerElemRootSet : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : CommRing S] [inst_3 : Algebra S R]
  (G : Type u_1) (H : Type u_2) [inst_4 : Monoid G] [inst_5 : MulSemiringAction G R] [inst_6 : SMulCommClass G S R]
  [inst_7 : Monoid H] [inst_8 : MulSemiringAction H R] [inst_9 : SMulCommClass H S R] [inst_10 : SMul G H]
  [IsScalarTower G H R] (f : Polynomial S), IsScalarTower G H ↑(f.rootSet R)
-- Mathlib.Data.ZMod.Coprime
/-- If `p` is a prime and `a` is an integer, then `a : ZMod p` is zero if and only if
`gcd a p ≠ 1`.  -/
ZMod.eq_zero_iff_gcd_ne_one : ∀ {a : ℤ} {p : ℕ} [pp : Fact (Nat.Prime p)], ↑a = 0 ↔ a.gcd ↑p ≠ 1
-- Init.PropLemmas
Decidable.not_imp_comm : ∀ {a b : Prop} [Decidable a] [Decidable b], ¬a → b ↔ ¬b → a
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
/-- The short complex `Hⁱ(G, X₂) ⟶ Hⁱ(G, X₃) ⟶ Hʲ(G, X₁)`.  -/
groupCohomology.mapShortComplex₃ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)} →
        X.ShortExact → {i j : ℕ} → i + 1 = j → CategoryTheory.ShortComplex (ModuleCat k)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
/-- The lattice invariant `g₃ := 140 G₆`.  -/
PeriodPair.g₃ : PeriodPair → ℂ
-- Mathlib.NumberTheory.ModularForms.QExpansion
/-- The analytic function `F` such that `f τ = F (exp (2 * π * I * τ / h))`, extended by a choice of
limit at `0`.
 -/
UpperHalfPlane.cuspFunction : ℝ → (UpperHalfPlane → ℂ) → ℂ → ℂ
-- Mathlib.Util.Notation3
Mathlib.Notation3.prettyPrintOpt : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
/-- If `i : X ⟶ Y` is a monomorphism of simplicial sets and `d : ℕ`, this is
the type of nondegenerate `d`-simplices of `Y` which do not belong to
the range of `i`.  -/
SSet.relativeCellComplexOfMono.Cell : {X Y : SSet} → (X ⟶ Y) → ℕ → Type u
-- Mathlib.LinearAlgebra.Contraction
dualTensorHom_prodMap_zero : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : Module R Q] (f : Module.Dual R M) (p : P),
  ((dualTensorHom R M P) (f ⊗ₜ[R] p)).prodMap 0 =
    (dualTensorHom R (M × N) (P × Q)) ((f ∘ₗ LinearMap.fst R M N) ⊗ₜ[R] (LinearMap.inl R P Q) p)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_of_mem_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : (a : α) → β a → Bool} {k : α}, k ∈ Std.ExtDTreeMap.filter f t → k ∈ t
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.toStructuredArrow_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (X : F.Elements),
  (CategoryTheory.CategoryOfElements.toStructuredArrow F).obj X =
    { left := { as := PUnit.unit }, right := X.fst, hom := TypeCat.ofHom fun x => X.snd }
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.Comonad.left_comparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R),
  R.comp (CategoryTheory.Comonad.comparison h) = h.toComonad.cofree
-- Mathlib.Algebra.Group.Subgroup.Map
/-- An additive subgroup is isomorphic to its image under an isomorphism. If you only
have an injective map, use `AddSubgroup.equivMapOfInjective`.  -/
AddEquiv.addSubgroupMap : {G : Type u_1} →
  {G' : Type u_2} →
    [inst : AddGroup G] → [inst_1 : AddGroup G'] → (e : G ≃+ G') → (H : AddSubgroup G) → ↥H ≃+ ↥(AddSubgroup.map (↑e) H)
-- Mathlib.Topology.QuasiSeparated
isQuasiSeparated_univ_iff : ∀ {α : Type u_3} [inst : TopologicalSpace α], IsQuasiSeparated Set.univ ↔ QuasiSeparatedSpace α
-- Mathlib.Order.CountableSupClosed
countableInfClosure_eq_sInter : ∀ {α : Type u_2} [inst : Preorder α] (s : Set α), countableInfClosure s = ⋂₀ {t | s ⊆ t ∧ CountableInfClosed t}
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.single_add : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M) (r₁ r₂ : R),
  AddMonoidAlgebra.single m (r₁ + r₂) = AddMonoidAlgebra.single m r₁ + AddMonoidAlgebra.single m r₂
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.singleton_span_isCompactElement : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M),
  IsCompactElement (R ∙ x)
-- Mathlib.NumberTheory.MulChar.Duality
/-- The group of `R`-valued multiplicative characters on a finite commutative monoid `M` is
(noncanonically) isomorphic to its unit group `Mˣ` when `R` is a ring that has enough roots
of unity.  -/
MulChar.mulEquiv_units : ∀ (M : Type u_1) (R : Type u_2) [inst : CommMonoid M] [inst_1 : CommRing R] [Finite M]
  [HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)], Nonempty (MulChar M R ≃* Mˣ)
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.codExtend'_target : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace Z] {s : Set B} (hs : IsOpen s) {proj : Z → ↑s} (e : Bundle.Trivialization F proj)
  [inst_3 : Nonempty (B → F → Z)],
  (Bundle.Trivialization.codExtend' hs e).target = Prod.map Subtype.val id '' e.toPretrivialization.target
-- Mathlib.Order.RelClasses
/-- The value from `WellFoundedGT.fix` is built from the successive ones as specified.  -/
WellFoundedGT.fix_eq : ∀ {α : Type u} [inst : LT α] [inst_1 : WellFoundedGT α] {motive : α → Sort u_1}
  (ind : (x : α) → ((y : α) → x < y → motive y) → motive x) (x : α),
  WellFoundedGT.fix ind x = ind x fun y x => WellFoundedGT.fix ind y
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetRing.mk : ∀ {α : Type u_1} {C : Set (Set α)},
  ∅ ∈ C →
    (∀ ⦃s t : Set α⦄, s ∈ C → t ∈ C → s ∪ t ∈ C) →
      (∀ ⦃s t : Set α⦄, s ∈ C → t ∈ C → s \ t ∈ C) → MeasureTheory.IsSetRing C
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Multipliable.div₀ : ∀ {α : Type u_1} {K : Type u_4} [inst : CommGroupWithZero K] [inst_1 : TopologicalSpace K] {f g : α → K}
  {L : SummationFilter α} [ContinuousInv₀ K] [ContinuousMul K],
  Multipliable f L → Multipliable g L → ∏'[L] (x : α), g x ≠ 0 → Multipliable (fun x => f x / g x) L
-- Mathlib.Data.Nat.Digits.Lemmas
_private.Mathlib.Data.Nat.Digits.Lemmas.0.List.alternatingSum.match_1.splitter : {G : Type u_1} →
  (motive : List G → Sort u_2) →
    (x : List G) →
      (Unit → motive []) → ((g : G) → motive [g]) → ((g h : G) → (t : List G) → motive (g :: h :: t)) → motive x
-- Mathlib.LinearAlgebra.FreeModule.PID
Submodule.comapSubtypeEquivOfLe.congr_simp : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {p q : Submodule R M} (hpq : p ≤ q), Submodule.comapSubtypeEquivOfLe hpq = Submodule.comapSubtypeEquivOfLe hpq
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Arg.fvar.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId fvarId_1 : Lean.FVarId),
  (Lean.Compiler.LCNF.Arg.fvar fvarId = Lean.Compiler.LCNF.Arg.fvar fvarId_1) = (fvarId = fvarId_1)
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasAntitoneBasis.mk : ∀ {α : Type u_1} {ι'' : Type u_6} [inst : Preorder ι''] {l : Filter α} {s : ι'' → Set α},
  l.HasBasis (fun x => True) s → Antitone s → l.HasAntitoneBasis s
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.nsmul_mem : ∀ {M : Type u_5} [inst : AddMonoid M] (S : AddSubmonoid M) {x : M}, x ∈ S → ∀ (n : ℕ), n • x ∈ S
-- Mathlib.Order.KrullDimension
Order.krullDim_le_one_iff_forall_isMax : ∀ {α : Type u_3} [inst : PartialOrder α] [inst_1 : OrderBot α], Order.krullDim α ≤ 1 ↔ ∀ (x : α), x ≠ ⊥ → IsMax x
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Basic.0.Std.Tactic.BVDecide.BVExpr.toString.match_1.eq_4 : ∀ (motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) (w : ℕ) (lhs : Std.Tactic.BVDecide.BVExpr w)
  (op : Std.Tactic.BVDecide.BVBinOp) (rhs : Std.Tactic.BVDecide.BVExpr w)
  (h_1 : (w idx : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var idx))
  (h_2 : (w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val))
  (h_3 :
    (len w start : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w) → motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr))
  (h_4 :
    (w : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinOp) → (rhs : Std.Tactic.BVDecide.BVExpr w) → motive w (lhs.bin op rhs))
  (h_5 :
    (w : ℕ) →
      (op : Std.Tactic.BVDecide.BVUnOp) →
        (operand : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op operand))
  (h_6 :
    (w l r : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr l) →
        (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h))
  (h_7 :
    (w w_1 n : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w_1) →
        (h : w = w_1 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h))
  (h_8 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs))
  (h_9 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs))
  (h_10 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)),
  (match w, lhs.bin op rhs with
    | w, Std.Tactic.BVDecide.BVExpr.var idx => h_1 w idx
    | w, Std.Tactic.BVDecide.BVExpr.const val => h_2 w val
    | len, Std.Tactic.BVDecide.BVExpr.extract start .(len) expr => h_3 len w start expr
    | w, lhs.bin op rhs => h_4 w lhs op rhs
    | w, Std.Tactic.BVDecide.BVExpr.un op operand => h_5 w op operand
    | w, lhs.append rhs h => h_6 w l r lhs rhs h
    | w, Std.Tactic.BVDecide.BVExpr.replicate n expr h => h_7 w w_1 n expr h
    | w, lhs.shiftLeft rhs => h_8 w n lhs rhs
    | w, lhs.shiftRight rhs => h_9 w n lhs rhs
    | w, lhs.arithShiftRight rhs => h_10 w n lhs rhs) =
    h_4 w lhs op rhs
-- Mathlib.Data.Fin.Embedding
Fin.addNatEmb_apply : ∀ {n : ℕ} (m : ℕ) (x : Fin n), (Fin.addNatEmb m) x = x.addNat m
-- Lean.Elab.Tactic.Grind.Basic
/-- Execute `x` with error recovery disabled  -/
Lean.Elab.Tactic.Grind.withoutRecover : {α : Type} → Lean.Elab.Tactic.Grind.GrindTacticM α → Lean.Elab.Tactic.Grind.GrindTacticM α
-- Init.Data.Nat.Lemmas
Nat.div_ne_zero_iff : ∀ {a b : ℕ}, a / b ≠ 0 ↔ b ≠ 0 ∧ b ≤ a
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.coe_adj : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (v w : ↑G'.verts), G'.coe.Adj v w = G'.Adj ↑v ↑w
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.ker_toSubmonoid : ∀ {G : Type u_1} [inst : Group G] {M : Type u_7} [inst_1 : MulOneClass M] (f : G →* M),
  f.ker.toSubmonoid = MonoidHom.mker f
-- Mathlib.Tactic.Determinant.Bird.Cert
/-- Certify the stop branch of `BirdDet.sumFrom`.

This corresponds to the `else 0` branch of:

```
sumFrom n lo f = if lo < n then f lo + sumFrom n (lo + 1) f else 0
```

Throws a meta-level error if called with `lo` such that `lo < ctx.dimension`.
 -/
Mathlib.Tactic.Determinant.certSumFromStop : {u : Lean.Level} →
  {α : Q(Type u)} →
    {rα : Q(CommRing «$α»)} → ℕ → Q(ℕ → «$α») → Mathlib.Tactic.Determinant.CertM rα (Mathlib.Tactic.Determinant.Cert rα)
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.precomposeInvEquiv.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} (α : F ≅ G) (c : CategoryTheory.Limits.Cocone F),
  CategoryTheory.Limits.IsColimit.precomposeInvEquiv α c =
    CategoryTheory.Limits.IsColimit.ofCoconeEquiv (CategoryTheory.Limits.Cocone.precomposeEquivalence α)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_filter_key_eq_size_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {f : α → Bool},
  (Std.DTreeMap.filter (fun k x => f k) t).size = t.size ↔ ∀ (k : α) (h : k ∈ t), f (t.getKey k h) = true
-- Lean.Parser.Do
Lean.Parser.Term.do.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Elab.App
/-- Return `some info` if we should elaborate as an eliminator.  -/
_private.Lean.Elab.App.0.Lean.Elab.Term.elabAppArgs.elabAsElim? : Lean.Expr →
  Array Lean.Elab.Term.NamedArg →
    Array Lean.Elab.Term.Arg → Bool → Bool → Lean.Elab.TermElabM (Option Lean.Elab.Term.ElabElimInfo)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas
Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go_Inv_of_Inv : ∀ (expr : Std.Tactic.BVDecide.BVLogicalExpr) (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit)
  (assign : Std.Tactic.BVDecide.BVExpr.Assignment) (cache : Std.Tactic.BVDecide.BVExpr.Cache aig),
  Std.Tactic.BVDecide.BVExpr.Cache.Inv assign aig cache →
    Std.Tactic.BVDecide.BVExpr.Cache.Inv assign
      (↑(Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go aig expr cache).result).aig
      (Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go aig expr cache).cache
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffWithinAt.congr_of_eventuallyEq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f f₁ : E → F} {x : E} {n : WithTop ℕ∞},
  ContDiffWithinAt 𝕜 n f s x → f₁ =ᶠ[nhdsWithin x s] f → f₁ x = f x → ContDiffWithinAt 𝕜 n f₁ s x
-- Mathlib.Algebra.Homology.Opposite
/-- Auxiliary definition for `unopEquivalence`.  -/
HomologicalComplex.unopFunctor : {ι : Type u_1} →
  (V : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_2} V] →
      (c : ComplexShape ι) →
        [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
          CategoryTheory.Functor (HomologicalComplex Vᵒᵖ c)ᵒᵖ (HomologicalComplex V c.symm)
-- Batteries.Lean.AttributeExtra
/-- A list of pre-tagged declarations with their values.  -/
Lean.ParametricAttributeExtra.base : {α : Type} → Lean.ParametricAttributeExtra α → Std.HashMap Lean.Name α
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.zipWithM.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (motive : List α → List β → Array γ → Sort u_4) (x : List α)
  (x_1 : List β) (acc : Array γ)
  (h_1 : (a : α) → (as : List α) → (b : β) → (bs : List β) → (acc : Array γ) → motive (a :: as) (b :: bs) acc)
  (h_2 : (x : List α) → (x_2 : List β) → (acc : Array γ) → motive x x_2 acc),
  (∀ (a : α) (as : List α) (b : β) (bs : List β), x = a :: as → x_1 = b :: bs → False) →
    (match x, x_1, acc with
      | a :: as, b :: bs, acc => h_1 a as b bs acc
      | x, x_3, acc => h_2 x x_3 acc) =
      h_2 x x_1 acc
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.measure_ne_top_of_subset : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α}, t ⊆ s → μ s ≠ ⊤ → μ t ≠ ⊤
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.resolvent_eq : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {a : A} {r : R}
  (h : r ∈ resolventSet R a), resolvent a r = ↑(IsUnit.unit h)⁻¹
-- Mathlib.Algebra.Order.Rearrangement
/-- **Equality case of the Rearrangement Inequality**: Pointwise multiplication of `f` and `g`,
which antivary together on `s`, is unchanged by a permutation if and only if `f ∘ σ` and `g`
antivary together on `s`. Stated by permuting the entries of `f`.  -/
AntivaryOn.sum_comp_perm_mul_eq_sum_mul_iff : ∀ {ι : Type u_1} {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α},
  AntivaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → (∑ i ∈ s, f (σ i) * g i = ∑ i ∈ s, f i * g i ↔ AntivaryOn (f ∘ ⇑σ) g ↑s)
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.forkOfKernelFork_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} {f g : X ⟶ Y}
  (c : CategoryTheory.Limits.KernelFork (f - g)),
  (CategoryTheory.Preadditive.forkOfKernelFork c).ι = CategoryTheory.Limits.Fork.ι c
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- The second projection from the product.  -/
CategoryTheory.SemiCartesianMonoidalCategory.snd : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    [self : CategoryTheory.SemiCartesianMonoidalCategory C] →
      (X Y : C) → CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Y
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.instAddCommGroup : {F : Type u} → [inst : Field F] → {W : WeierstrassCurve.Jacobian F} → AddCommGroup W.Point
-- Mathlib.Algebra.Homology.HomologicalBicomplex
HomologicalComplex₂.flipEquivalenceUnitIso_inv_app_f_f : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (X : HomologicalComplex₂ C c₁ c₂)
  (i : I₁) (i_1 : I₂),
  (((HomologicalComplex₂.flipEquivalenceUnitIso C c₁ c₂).inv.app X).f i).f i_1 =
    CategoryTheory.CategoryStruct.id ((X.X i).X i_1)
-- Mathlib.RingTheory.Idempotents
Subsemigroup.mem_corner_iff_mul_right : ∀ {R : Type u_1} {e : R} [inst : Semigroup R],
  IsIdempotentElem e → IsMulCentral e → ∀ {r : R}, r ∈ Subsemigroup.corner e ↔ r * e = r
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_diff!_of_contains_eq_false_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β},
        Std.DTreeMap.Internal.Impl.contains k m₂ = false →
          Std.DTreeMap.Internal.Impl.Const.getD (m₁.diff! m₂) k fallback =
            Std.DTreeMap.Internal.Impl.Const.getD m₁ k fallback
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  (Std.TreeMap.Raw.unitOfList l cmp).contains k = l.contains k
-- Init.Grind.FieldNormNum
Lean.Grind.Field.NormNum.ofRat_inv : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] (a : ℚ),
  Lean.Grind.Field.NormNum.ofRat a⁻¹ = (Lean.Grind.Field.NormNum.ofRat a)⁻¹
-- Init.SizeOf
Bool.true.sizeOf_spec : sizeOf true = 1
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.Stream.cons.injEq : ∀ {α : Type u_1} (v : α) (r : RBTree.RBNode α) (tail : RBTree.RBNode.Stream α) (v_1 : α) (r_1 : RBTree.RBNode α)
  (tail_1 : RBTree.RBNode.Stream α),
  (RBTree.RBNode.Stream.cons v r tail = RBTree.RBNode.Stream.cons v_1 r_1 tail_1) = (v = v_1 ∧ r = r_1 ∧ tail = tail_1)
-- Mathlib.Algebra.Polynomial.RingDivision
Polynomial.irreducible_C_mul_X_add_C : ∀ {R : Type u} [inst : CommRing R] [IsDomain R] {a b : R},
  a ≠ 0 → IsRelPrime a b → Irreducible (Polynomial.C a * Polynomial.X + Polynomial.C b)
-- Mathlib.Order.Minimal
/-- **Alias** of `image_monotone_setOfPred_maximal`. -/
image_monotone_setOf_maximal : ∀ {α : Type u_2} {β : Type u_3} {P : α → Prop} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  (∀ ⦃y x : α⦄, P y → P x → (f y ≤ f x ↔ y ≤ x)) →
    f '' {x | Maximal P x} = {x | Maximal (fun x => ∃ x₀, P x₀ ∧ f x₀ = x) x}
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.replayConsts.replayKernel.unsafe_1 : Lean.Kernel.Environment →
  Lean.Kernel.Environment →
    List Lean.AsyncConst✝ →
      Lean.EnvExtension Lean.EnvExtensionState →
        Lean.Kernel.Environment → Lean.ReplayFn Lean.EnvExtensionState → Array Lean.EnvExtensionState