mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.core0.sizeOf_spec : ∀ (a zero : Lean.Expr), sizeOf (Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.core0 a zero) = 1 + sizeOf a + sizeOf zero
-- Batteries.Data.Random.MersenneTwister
Batteries.Random.MersenneTwister.Config.mk.inj : ∀ {wordSize stateSize : ℕ} {shiftSize : Fin stateSize} {maskBits : Fin wordSize} {xorMask : BitVec wordSize}
  {temperingShifts : ℕ × ℕ × ℕ × ℕ} {temperingMasks : BitVec wordSize × BitVec wordSize × BitVec wordSize}
  {initMult initSeed : BitVec wordSize} {wordSize_1 stateSize_1 : ℕ} {shiftSize_1 : Fin stateSize_1}
  {maskBits_1 : Fin wordSize_1} {xorMask_1 : BitVec wordSize_1} {temperingShifts_1 : ℕ × ℕ × ℕ × ℕ}
  {temperingMasks_1 : BitVec wordSize_1 × BitVec wordSize_1 × BitVec wordSize_1}
  {initMult_1 initSeed_1 : BitVec wordSize_1},
  { wordSize := wordSize, stateSize := stateSize, shiftSize := shiftSize, maskBits := maskBits, xorMask := xorMask,
        temperingShifts := temperingShifts, temperingMasks := temperingMasks, initMult := initMult,
        initSeed := initSeed } =
      { wordSize := wordSize_1, stateSize := stateSize_1, shiftSize := shiftSize_1, maskBits := maskBits_1,
        xorMask := xorMask_1, temperingShifts := temperingShifts_1, temperingMasks := temperingMasks_1,
        initMult := initMult_1, initSeed := initSeed_1 } →
    wordSize = wordSize_1 ∧
      stateSize = stateSize_1 ∧
        shiftSize ≍ shiftSize_1 ∧
          maskBits ≍ maskBits_1 ∧
            xorMask ≍ xorMask_1 ∧
              temperingShifts = temperingShifts_1 ∧
                temperingMasks ≍ temperingMasks_1 ∧ initMult ≍ initMult_1 ∧ initSeed ≍ initSeed_1
-- Init.Data.Iterators.Lemmas.Combinators.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Take.0.Std.IterM.step_take.match_1.eq_3 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (h : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.done, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_3 h
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.cancel_natIso_inv_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ≅ G) {X : C} {Y : D} (g g' : F.obj X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (α.inv.app X) g = CategoryTheory.CategoryStruct.comp (α.inv.app X) g' ↔ g = g'
-- Mathlib.Algebra.GroupWithZero.Associated
Irreducible.dvd_or_isRelPrime : ∀ {M : Type u_1} [inst : Monoid M] {p n : M}, Irreducible p → p ∣ n ∨ IsRelPrime p n
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.LiftRelO.imp : ∀ {α : Type u} {β : Type v} {R S : α → β → Prop} {C D : Stream'.WSeq α → Stream'.WSeq β → Prop},
  (∀ (a : α) (b : β), R a b → S a b) →
    (∀ (s : Stream'.WSeq α) (t : Stream'.WSeq β), C s t → D s t) →
      ∀ {o : Option (α × Stream'.WSeq α)} {p : Option (β × Stream'.WSeq β)},
        Stream'.WSeq.LiftRelO R C o p → Stream'.WSeq.LiftRelO S D o p
-- Init.Data.Int.DivMod.Lemmas
Int.bmod_eq_bmod_iff_bmod_sub_eq_zero : ∀ {m : ℤ} {n : ℕ} {k : ℤ}, m.bmod n = k.bmod n ↔ (m - k).bmod n = 0
-- Mathlib.LinearAlgebra.Projectivization.Action
/-- Any group acting `K`-linearly on `V` (such as the general linear group) acts on `ℙ V`.  -/
Projectivization.instMulAction : {G : Type u_1} →
  {K : Type u_2} →
    {V : Type u_3} →
      [inst : AddCommGroup V] →
        [inst_1 : DivisionRing K] →
          [inst_2 : Module K V] →
            [inst_3 : Group G] →
              [inst_4 : DistribMulAction G V] → [SMulCommClass G K V] → MulAction G (Projectivization K V)
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.IsTrivial.trivialOn : ∀ {α : Type u_1} {f : Set α}, f.Nonempty → (Hypergraph.trivialOn f).IsTrivial
-- Mathlib.Analysis.Complex.Arg
Complex.sameRay_iff_arg_div_eq_zero : ∀ {x y : ℂ}, SameRay ℝ x y ↔ (x / y).arg = 0
-- Mathlib.Analysis.Calculus.LogDeriv
logDeriv_fun_pow : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {f : 𝕜 → 𝕜'} {x : 𝕜},
  DifferentiableAt 𝕜 f x → ∀ (n : ℕ), logDeriv (fun x => f x ^ n) x = ↑n * logDeriv f x
-- Mathlib.Probability.Kernel.CondDistrib
/-- If the singleton `{x}` has non-zero mass for `μ.map X`, then for all `s : Set Ω`,
`condDistrib Y X μ x s = (μ.map X {x})⁻¹ * μ.map (fun a => (X a, Y a)) ({x} ×ˢ s)` .  -/
ProbabilityTheory.condDistrib_apply_of_ne_zero : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_3 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β}
  [MeasurableSingletonClass β],
  Measurable Y →
    ∀ (x : β),
      (MeasureTheory.Measure.map X μ) {x} ≠ 0 →
        ∀ (s : Set Ω),
          ((ProbabilityTheory.condDistrib Y X μ) x) s =
            ((MeasureTheory.Measure.map X μ) {x})⁻¹ * (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ) ({x} ×ˢ s)
-- Mathlib.CategoryTheory.Functor.Basic
CategoryTheory.Functor.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : SizeOf C] [inst_3 : SizeOf D] (obj : C → D) (map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y))
  (map_id :
    autoParam (∀ (X : C), map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (obj X))
      CategoryTheory.Functor.map_id._autoParam)
  (map_comp :
    autoParam
      (∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
        map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (map f) (map g))
      CategoryTheory.Functor.map_comp._autoParam),
  sizeOf { obj := obj, map := map, map_id := map_id, map_comp := map_comp } = 1
-- Mathlib.Computability.RegularExpressions
RegularExpression.map.eq_5 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (P Q : RegularExpression α),
  RegularExpression.map f (P.comp Q) = RegularExpression.map f P * RegularExpression.map f Q
-- Mathlib.Algebra.Homology.BifunctorShift
CategoryTheory.Functor.instCommShiftCochainComplexIntMapFlipMap₂CochainComplex : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  [inst_3 : CategoryTheory.Preadditive C₁] [inst_4 : CategoryTheory.Preadditive C₂]
  [inst_5 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  [inst_6 : F.Additive] [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive]
  [inst_8 : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F]
  {K₂ L₂ : CochainComplex C₂ ℤ} (g : K₂ ⟶ L₂), CategoryTheory.NatTrans.CommShift (F.map₂CochainComplex.flip.map g) ℤ
-- Mathlib.Topology.Compactness.Compact
/-- If values of `f : Y → X` belong to a compact set `s` eventually along a filter `l`
and `y` is a unique `MapClusterPt` for `f` along `l` in `s`,
then `f` tends to `𝓝 y` along `l`.  -/
IsCompact.tendsto_nhds_of_unique_mapClusterPt : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {Y : Type u_2} {l : Filter Y} {y : X} {f : Y → X},
  IsCompact s → (∀ᶠ (x : Y) in l, f x ∈ s) → (∀ x ∈ s, MapClusterPt x l f → x = y) → Filter.Tendsto f l (nhds y)
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.sMod_nonneg : ∀ (p : ℕ), p ≠ 0 → ∀ (i : ℕ), 0 ≤ LucasLehmer.sMod p i
-- Mathlib.CategoryTheory.Filtered.Basic
/-- For every universe `w`, `C` is filtered if and only if every finite diagram in `C` with shape
in `w` admits a cocone.  -/
CategoryTheory.IsCofiltered.iff_cone_nonempty : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.IsCofiltered C ↔
    ∀ {J : Type w} [inst_1 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J]
      (F : CategoryTheory.Functor J C), Nonempty (CategoryTheory.Limits.Cone F)
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.inv_cpow : ∀ (x n : ℂ), x.arg ≠ Real.pi → x⁻¹ ^ n = (x ^ n)⁻¹
-- Std.Time.Date.ValidDate
Std.Time.Internal.Bounded.LE.mk.congr_simp : ∀ {lo hi : ℤ} (val val_1 : ℤ) (e_val : val = val_1) (proof : lo ≤ val ∧ val ≤ hi),
  Std.Time.Internal.Bounded.LE.mk val proof = Std.Time.Internal.Bounded.LE.mk val_1 ⋯
-- Mathlib.Order.Antisymmetrization
Relation.SymmGen.of_gt : ∀ {α : Type u_1} {a b : α} [inst : Preorder α], b < a → Relation.SymmGen (fun x1 x2 => x1 ≤ x2) a b
-- Mathlib.FieldTheory.IsAlgClosed.Basic
/-- Over an algebraically closed field of characteristic zero a necessary and sufficient condition
for the set of roots of a nonzero polynomial `f` to be a subset of the set of roots of `g` is that
`f` divides `f.derivative * g`. Over an integral domain, this is a sufficient but not necessary
condition. See `isRoot_of_isRoot_of_dvd_derivative_mul`  -/
Polynomial.isRoot_of_isRoot_iff_dvd_derivative_mul : ∀ {K : Type u_1} [inst : Field K] [IsAlgClosed K] [CharZero K] {f g : Polynomial K},
  f ≠ 0 → ((∀ (x : K), f.IsRoot x → g.IsRoot x) ↔ f ∣ Polynomial.derivative f * g)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
eisensteinSeries.eq_1 : ∀ {N : ℕ} (a : Fin 2 → ZMod N) (k : ℤ) (z : UpperHalfPlane),
  eisensteinSeries a k z = ∑' (x : ↑(EisensteinSeries.gammaSet N 1 a)), EisensteinSeries.eisSummand k (↑x) z
-- Mathlib.Topology.Order
Nat.cast_continuous : ∀ {R : Type u_1} [inst : NatCast R] [inst_1 : TopologicalSpace R], Continuous Nat.cast
-- Mathlib.Tactic.DefEqAbuse
/-- Recursively modify the pp options captured in `MessageData.withContext` nodes.
Used to re-render `X =?= X` failures with `pp.universes` or `pp.explicit` to show
the difference between LHS and RHS without re-running the full analysis.  -/
_private.Mathlib.Tactic.DefEqAbuse.0.Lean.MessageData.withPPOptions : Lean.MessageData → (Lean.Options → Lean.Options) → Lean.MessageData
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.add_one_le_succ : ∀ (c : Cardinal.{u_1}), c + 1 ≤ Order.succ c
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_left' : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f],
  CategoryTheory.Limits.HasLimit
    (CategoryTheory.Limits.cospan
      (((CategoryTheory.Limits.cospan f g).comp AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace).map
        CategoryTheory.Limits.WalkingCospan.Hom.inl)
      (((CategoryTheory.Limits.cospan f g).comp AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace).map
        CategoryTheory.Limits.WalkingCospan.Hom.inr))
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.instMul : {q : ℕ} → Mul (LucasLehmer.X q)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- The fundamental property of the operator norm of a continuous multilinear map:
`‖f m‖` is bounded by `‖f‖` times the product of the `‖m i‖`.  -/
ContinuousMultilinearMap.le_opNorm : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {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 : Fintype ι]
  (f : ContinuousMultilinearMap 𝕜 E G) (m : (i : ι) → E i), ‖f m‖ ≤ ‖f‖ * ∏ i, ‖m i‖
-- Mathlib.GroupTheory.Commutator.Basic
addCommutator_eq_bot : ∀ (G : Type u_1) [inst : AddGroup G] [hG : IsAddCommutative G], addCommutator G = ⊥
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.associator_naturality_assoc : ∀ {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) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  {X₁ X₂ X₃ Y₁ Y₂ Y₃ : CategoryTheory.LocalizedMonoidal L W ε} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃)
  {Z : CategoryTheory.LocalizedMonoidal L W ε}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₂ Y₃) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂) f₃)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y₁ Y₂ Y₃).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ X₃).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ (CategoryTheory.MonoidalCategoryStruct.tensorHom f₂ f₃)) h)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.subtype_apply : ∀ {R : Type u} {M : Type v} [inst : VAdd R M] {p : SubAddAction R M} (x : ↥p), p.subtype x = ↑x
-- Mathlib.SetTheory.ZFC.Basic
/-- Turns a binary definable function into a binary `PSet` function.  -/
ZFSet.Definable₂.out : (f : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}) → [ZFSet.Definable₂ f] → PSet.{u} → PSet.{u} → PSet.{u}
-- Mathlib.Order.SuccPred.LinearLocallyFinite
LinearOrder.isSuccArchimedean_of_isPredArchimedean : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : PredOrder ι] [IsPredArchimedean ι],
  IsSuccArchimedean ι
-- Lean.DocString.Markdown
Lean.Doc.instToMarkdownPartOfMarkdownInlineOfMarkdownBlock : {i : Type u_1} →
  {b : Type u_2} →
    {p : Type u_3} →
      [Lean.Doc.MarkdownInline i] → [Lean.Doc.MarkdownBlock i b] → Lean.Doc.ToMarkdown (Lean.Doc.Part i b p)
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.intCast : ∀ (K : Type u) [inst : CommRing K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p] (x : ℤ),
  ↑x = PerfectClosure.mk K p (0, ↑x)
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.le_opNorm_mul_pow_of_le : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  (f : E [⋀^Fin n]→L[𝕜] F) {m : Fin n → E} {b : ℝ}, ‖m‖ ≤ b → ‖f m‖ ≤ ‖f‖ * b ^ n
-- Init.Coe
/-- `CoeFun α (γ : α → Sort v)` is a coercion to a function. `γ a` should be a
(coercion-to-)function type, and this is triggered whenever an element
`f : α` appears in an application like `f x`, which would not make sense since
`f` does not have a function type.
`CoeFun` instances apply to `CoeOut` as well.
 -/
CoeFun : (α : Sort u) → outParam (α → Sort v) → Sort (max (max 1 u) v)
-- Mathlib.Data.Sym.NatCard
Sym2.instInfiniteSubtypeIsDiag : ∀ (α : Type u_1) [Infinite α], Infinite { a // a.IsDiag }
-- Std.Data.ExtDHashMap.Basic
Std.ExtDHashMap.instUnionOfEquivBEqOfLawfulHashable : {α : Type u} →
  {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Union (Std.ExtDHashMap α β)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.chainsMap_f_map_mono : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B),
  Function.Injective ⇑f → ∀ [CategoryTheory.Mono φ] (i : ℕ), CategoryTheory.Mono ((groupHomology.chainsMap f φ).f i)
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.forIn'_eq_foldlM.match_1.splitter : {β : Type u_1} →
  (motive : ForInStep β → Sort u_2) →
    (b : ForInStep β) → ((b : β) → motive (ForInStep.yield b)) → ((b : β) → motive (ForInStep.done b)) → motive b
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.le_of_le_graph : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {f g : E →ₗ.[R] F}, f.graph ≤ g.graph → f ≤ g
-- Aesop.Builder.Forward
Aesop.RuleBuilder.getForwardIndexingMode : Lean.Expr → Aesop.UnorderedArraySet Aesop.PremiseIndex → Lean.MetaM Aesop.IndexingMode
-- Mathlib.Algebra.Group.Action.Opposite
AddMonoid.toOppositeAddAction.eq_1 : ∀ {α : Type u_3} [inst : AddMonoid α],
  AddMonoid.toOppositeAddAction = { toVAdd := Add.toVAddAddOpposite α, add_vadd := ⋯, zero_vadd := ⋯ }
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_eq_some_getValue : ∀ {α : Type u} {β : Type v} [inst : BEq α] {l : List ((_ : α) × β)} {a : α}
  (h : Std.Internal.List.containsKey a l = true),
  Std.Internal.List.getValue? a l = some (Std.Internal.List.getValue a l h)
-- Init.Prelude
Lean.ParserDescr.brecOn.go : {motive : Lean.ParserDescr → Sort u} →
  (t : Lean.ParserDescr) →
    ((t : Lean.ParserDescr) → Lean.ParserDescr.below t → motive t) → motive t ×' Lean.ParserDescr.below t
-- Init.Ext
/-- Apply a single extensionality theorem to the current goal.  -/
Lean.Elab.Tactic.Ext.applyExtTheorem : Lean.ParserDescr
-- Mathlib.Analysis.Calculus.ContDiff.Operations
contDiff_pi : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {n : WithTop ℕ∞} {ι : Type u_3} [inst_3 : Fintype ι] {F' : ι → Type u_5}
  [inst_4 : (i : ι) → NormedAddCommGroup (F' i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i},
  ContDiff 𝕜 n Φ ↔ ∀ (i : ι), ContDiff 𝕜 n fun x => Φ x i
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.range_sin_infinite : (Set.range Real.sin).Infinite
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousMonoidHom.instCompactSpace : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] [DiscreteTopology A] [ContinuousMul B] [T2Space B] [CompactSpace B],
  CompactSpace (A →ₜ* B)
-- Init.Data.Array.Lemmas
Array.exists_push_of_size_pos : ∀ {α : Type u_1} {xs : Array α}, 0 < xs.size → ∃ ys a, xs = ys.push a
-- Std.Data.ExtTreeMap.Basic
Std.ExtTreeMap.instReflBEq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : BEq β] [ReflBEq β],
  ReflBEq (Std.ExtTreeMap α β cmp)
-- Mathlib.Topology.Covering.Basic
IsCoveringMapOn.homeomorph_comp : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {s : Set X},
  IsCoveringMapOn f s →
    ∀ {Y : Type u_3} [inst_2 : TopologicalSpace Y] (g : X ≃ₜ Y), IsCoveringMapOn (⇑g ∘ f) (⇑g.symm ⁻¹' s)
-- Init.Core
/-- Non-dependent eliminator for `Iff`.  -/
Iff.elim : {a b : Prop} → {α : Sort u_1} → ((a → b) → (b → a) → α) → (a ↔ b) → α
-- Mathlib.Algebra.Quaternion
Quaternion.im_natCast : ∀ {R : Type u_3} [inst : CommRing R] (n : ℕ), (↑n).im = 0
-- Mathlib.Topology.Algebra.Group.Basic
nhds_translation_neg_add : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] (x : G),
  Filter.comap (fun x_1 => -x + x_1) (nhds 0) = nhds x
-- Mathlib.SetTheory.Cardinal.ENat
/-- The coercion `Cardinal.ofENat` and the projection `Cardinal.toENat` form a Galois connection.
See also `Cardinal.gciENat`.  -/
Cardinal.enat_gc : GaloisConnection Cardinal.ofENat ⇑Cardinal.toENat
-- Mathlib.Order.Ideal
Order.Ideal.ext_iff : ∀ {P : Type u_1} [inst : LE P] {s t : Order.Ideal P}, s = t ↔ ↑s = ↑t
-- Mathlib.Data.Matrix.Diagonal
Matrix.one_eq_pi_single : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : One α] {i j : n},
  1 i j = Pi.single i 1 j
-- Mathlib.Algebra.Symmetrized
SymAlg.sym_mul_self : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : Invertible 2] (a : α), SymAlg.sym (a * a) = SymAlg.sym a * SymAlg.sym a
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.BlockMem.eq_1 : ∀ (G : Type u_1) [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] (a : X),
  MulAction.BlockMem G a = { B // a ∈ B ∧ MulAction.IsBlock G B }
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.bind₁_comp_rename : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [inst : CommSemiring R] {υ : Type u_6} (f : τ → MvPolynomial υ R)
  (g : σ → τ), (MvPolynomial.bind₁ f).comp (MvPolynomial.rename g) = MvPolynomial.bind₁ (f ∘ g)
-- Mathlib.Analysis.Complex.Isometry
/-- The determinant of `rotation` (as a linear map) is equal to `1`.  -/
det_rotation : ∀ (a : Circle), LinearMap.det ↑(rotation a).toLinearEquiv = 1
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If `r` is a positive constant, `fun x ↦ f x / r` tends to negative infinity along a filter
if and only if `f` tends to negative infinity along the same filter.  -/
Filter.tendsto_div_const_atBot_of_pos : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α}, 0 < r → (Filter.Tendsto (fun x => f x / r) l Filter.atBot ↔ Filter.Tendsto f l Filter.atBot)
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.residue_surjective : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R], Function.Surjective ⇑(IsLocalRing.residue R)
-- Mathlib.Data.Fin.SuccPred
/-- The `Fin.le_zero_iff` in `Lean` only applies in `Fin (n+1)`.
This one instead uses a `NeZero n` typeclass hypothesis.
 -/
Fin.le_zero_iff' : ∀ {n : ℕ} [inst : NeZero n] {k : Fin n}, k ≤ 0 ↔ k = 0
-- Mathlib.Algebra.Order.Rearrangement
/-- **Equality case of the Rearrangement Inequality**: Pointwise multiplication of `f` and `g`,
which monovary together on `s`, is unchanged by a permutation if and only if `f` and `g ∘ σ`
monovary together on `s`. Stated by permuting the entries of `g`.  -/
MonovaryOn.sum_mul_comp_perm_eq_sum_mul_iff : ∀ {ι : Type u_1} {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α},
  MonovaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → (∑ i ∈ s, f i * g (σ i) = ∑ i ∈ s, f i * g i ↔ MonovaryOn f (g ∘ ⇑σ) ↑s)
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_hom_app_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.Additive] (K : CochainComplex C ℤ) (n i : ℤ),
  ((CategoryTheory.Functor.commShiftIso (F.mapHomologicalComplex (ComplexShape.up ℤ)) n).hom.app K).f i =
    CategoryTheory.CategoryStruct.id
      ((((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).comp
                (F.mapHomologicalComplex (ComplexShape.up ℤ))).obj
            K).X
        i)
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.isoOfHom_inv_hom_id : ∀ {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) [inst_2 : L.IsLocalization W] {X Y : C} (f : X ⟶ Y) (hf : W f),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.isoOfHom L W f hf).inv (L.map f) =
    CategoryTheory.CategoryStruct.id (L.obj Y)
-- Mathlib.Algebra.DirectSum.Ring
/-- If two ring homomorphisms from `⨁ i, A i` are equal on each `of A i y`,
then they are equal.

See note [partially-applied ext lemmas].  -/
DirectSum.ringHom_ext' : ∀ {ι : Type u_1} [inst : DecidableEq ι] {A : ι → Type u_2} {R : Type u_3} [inst_1 : (i : ι) → AddCommMonoid (A i)]
  [inst_2 : AddMonoid ι] [inst_3 : DirectSum.GSemiring A] [inst_4 : Semiring R]
  ⦃F G : (DirectSum ι fun i => A i) →+* R⦄,
  (∀ (i : ι), (↑F).comp (DirectSum.of A i) = (↑G).comp (DirectSum.of A i)) → F = G