mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
/-- The triangle in the standard simplex with vertices `a`, `b`, and `c`.  -/
SSet.stdSimplex.triangle : {n : ℕ} → (a b c : Fin (n + 1)) → a ≤ b → b ≤ c → (SSet.stdSimplex.obj { len := n }).obj (Opposite.op { len := 2 })
-- Mathlib.Order.Filter.IsBounded
Filter.isBoundedUnder_of_eventually_le : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] {f : Filter β} {u : β → α} {a : α},
  (∀ᶠ (x : β) in f, u x ≤ a) → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint.match_3.congr_eq_3 : ∀ {n : ℕ} (motive : Option (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)) → Sort u_1)
  (x : Option (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)))
  (h_1 : (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → motive (some (some c)))
  (h_2 : Unit → motive (some none)) (h_3 : Unit → motive none),
  x = none →
    (match x with
      | some (some c) => h_1 c
      | some none => h_2 ()
      | none => h_3 ()) ≍
      h_3 ()
-- Mathlib.Data.ENat.Basic
/-- **Alias** of `ENat.natCast_inj`. -/
ENat.coe_inj : ∀ {a b : ℕ}, ↑a = ↑b ↔ a = b
-- Mathlib.Algebra.Group.Basic
pow_mul_pow_eq_one : ∀ {M : Type u_4} [inst : Monoid M] {a b : M} (n : ℕ), a * b = 1 → a ^ n * b ^ n = 1
-- Mathlib.Logic.Relation
Relation.ReflTransGen.trans_induction_on : ∀ {α : Type u_1} {r : α → α → Prop} {motive : {a b : α} → Relation.ReflTransGen r a b → Prop} {a b : α}
  (h : Relation.ReflTransGen r a b),
  (∀ (a : α), motive ⋯) →
    (∀ {a b : α} (h : r a b), motive ⋯) →
      (∀ {a b c : α} (h₁ : Relation.ReflTransGen r a b) (h₂ : Relation.ReflTransGen r b c),
          motive h₁ → motive h₂ → motive ⋯) →
        motive h
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k fallback : α}, k ∉ t₁ → (t₁ ∪ t₂).getKeyD k fallback = t₂.getKeyD k fallback
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
HasProd.of_nat_of_neg : ∀ {G : Type u_2} [inst : CommGroup G] {g g' : G} [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] {f : ℤ → G},
  HasProd (fun n => f ↑n) g → HasProd (fun n => f (-↑n)) g' → HasProd f (g * g' / f 0)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
/-- Eta-expanded form of `MeasureTheory.lintegral_indicator_one₀` -/
MeasureTheory.lintegral_indicator_fun_one₀ : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.NullMeasurableSet s μ → ∫⁻ (a : α), s.indicator (fun x => 1) a ∂μ = μ s
-- Mathlib.Control.ULift
/-- Applicative sequencing.  -/
ULift.seq : {α : Type u_1} → {β : Type u_2} → ULift.{u_3, max u_1 u_2} (α → β) → (Unit → ULift.{u_4, u_1} α) → ULift.{u, u_2} β
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxi.Iterator.isSome_next_of_isPlausibleIndirectOutput : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] {it : Std.Iter α} {out : α},
  it.IsPlausibleIndirectOutput out → it.internalState.next.isSome = true
-- Mathlib.Algebra.Ring.Basic
/-- In a ring, `IsCancelMulZero` and `NoZeroDivisors` are equivalent.  -/
isCancelMulZero_iff_noZeroDivisors : ∀ {R : Type u_3} [inst : NonUnitalNonAssocRing R], IsCancelMulZero R ↔ NoZeroDivisors R
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.prod_mahlerMeasure_eq_mahlerMeasure_prod : ∀ (s : Multiset (Polynomial ℂ)), s.prod.mahlerMeasure = (Multiset.map (fun p => p.mahlerMeasure) s).prod
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.expEquiv_symm : ∀ {G : Type u_5} [inst : AddGroup G], WithZero.expEquiv.symm = WithZero.logEquiv
-- Mathlib.NumberTheory.Padics.Measure.Basic
AbstractMeasure.contractFst_apply : ∀ {X : Type u_1} {Y : Type u_2} {R : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : CommRing R] [inst_3 : TopologicalSpace R] [inst_4 : IsTopologicalRing R] (μ : AbstractMeasure X R R)
  (f : C(X × Y, R)) (y : Y),
  ((AbstractMeasure.contractFst μ) f) y = μ { toFun := fun x => f (x, y), continuous_toFun := ⋯ }
-- Mathlib.Order.OmegaCompletePartialOrder
/-- **Alias** of the forward direction of `OmegaCompletePartialOrder.ωScottContinuous_iff_map_ωSup_of_orderHom`.

---

A monotone function `f : α →o β` is ωScott continuous if and only if it distributes over ωSup.  -/
OmegaCompletePartialOrder.ωScottContinuous.map_ωSup_of_orderHom : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
  {f : α →o β},
  OmegaCompletePartialOrder.ωScottContinuous ⇑f →
    ∀ (c : OmegaCompletePartialOrder.Chain α),
      f (OmegaCompletePartialOrder.ωSup c) = OmegaCompletePartialOrder.ωSup (c.map f)
-- Lean.Widget.TaggedText
Lean.Widget.instReprTaggedText.repr : {α : Type u_1} → [Repr α] → Lean.Widget.TaggedText α → ℕ → Std.Format
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.CaseTrace.num : Lean.Meta.Grind.CaseTrace → ℕ
-- Mathlib.RingTheory.Valuation.Integers
Valuation.Integers.isUnit_iff_valuation_eq_one : ∀ {F : Type u} {Γ₀ : Type v} [inst : Field F] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀}
  {O : Type w} [inst_2 : CommRing O] [inst_3 : Algebra O F],
  v.Integers O → ∀ {x : O}, IsUnit x ↔ v ((algebraMap O F) x) = 1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.insert! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k : α} {v : β k},
          (Std.DTreeMap.Internal.Impl.insert! k v t₁).Equiv (Std.DTreeMap.Internal.Impl.insert! k v t₂)
-- Init.Data.Nat.Lemmas
Nat.pow_le_one_iff : ∀ {n a : ℕ}, n ≠ 0 → (a ^ n ≤ 1 ↔ a ≤ 1)
-- Mathlib.Data.Finsupp.Defs
Finsupp.support_onFinset : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] [inst_1 : DecidableEq M] {s : Finset α} {f : α → M}
  (hf : ∀ (a : α), f a ≠ 0 → a ∈ s), (Finsupp.onFinset s f hf).support = {a ∈ s | f a ≠ 0}
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The minimal distance of a point to a set containing it vanishes.  -/
Metric.infDist_zero_of_mem : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x : α}, x ∈ s → Metric.infDist x s = 0
-- Mathlib.CategoryTheory.Sites.Descent.Precoverage
/-- If `F` is a prestack for a Grothendieck topology `J` and `F` is a stack
for a covering sieve `R`, then it is also a stack for `R'` if `R ≤ R'`.  -/
CategoryTheory.Pseudofunctor.IsStackFor.of_le' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {S : C}
  {R : CategoryTheory.Sieve S},
  F.IsStackFor R.arrows →
    ∀ {J : CategoryTheory.GrothendieckTopology C},
      R ∈ J S → ∀ [F.IsPrestack J] {R' : CategoryTheory.Sieve S}, R ≤ R' → F.IsStackFor R'.arrows
-- Mathlib.Analysis.Calculus.FDeriv.Add
DifferentiableAt.add_iff_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {x : E}, DifferentiableAt 𝕜 f x → (DifferentiableAt 𝕜 (f + g) x ↔ DifferentiableAt 𝕜 g x)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inv_zero : ∀ {R : Type u} {M : Type v} [inst : DivisionSemiring R] [inst_1 : AddCommGroup M] [inst_2 : Module Rᵐᵒᵖ M]
  [inst_3 : Module R M], 0⁻¹ = 0
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.CosimplicialObject.equivalenceLeftToRight_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 :
    ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
      CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom]
  (F : CategoryTheory.Arrow C) (X : CategoryTheory.CosimplicialObject.Augmented C) (G : F.augmentedCechConerve ⟶ X),
  (CategoryTheory.CosimplicialObject.equivalenceLeftToRight F X G).left = G.left
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.restrictHom_smul_under : ∀ (G : Type u_1) (G' : Type u_2) [inst : Group G] [inst_1 : Group G'] (A : Type u_5) (B : Type u_6) (C : Type u_7)
  [inst_2 : CommRing A] [inst_3 : CommRing B] [inst_4 : CommRing C] [inst_5 : IsDomain C] [inst_6 : Algebra A B]
  [inst_7 : Algebra A C] [inst_8 : Algebra B C] [inst_9 : FaithfulSMul A B] [inst_10 : FaithfulSMul B C]
  [inst_11 : IsScalarTower A B C] [inst_12 : Finite G] [inst_13 : Finite G'] [inst_14 : MulSemiringAction G C]
  [inst_15 : IsGaloisGroup G A C] [inst_16 : MulSemiringAction G' B] [inst_17 : IsGaloisGroup G' A B] (g : G)
  (I : Ideal C), (IsGaloisGroup.restrictHom G G' A B C) g • Ideal.under B I = Ideal.under B (g • I)
-- Mathlib.Topology.GDelta.Basic
/-- The preimage of a Gδ set under a continuous map is Gδ.  -/
IsGδ.preimage : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set Y},
  Continuous f → IsGδ s → IsGδ (f ⁻¹' s)
-- Mathlib.NumberTheory.LSeries.HurwitzZetaValues
/-- Reformulation of `cosZeta_two_mul_nat` using `Gammaℂ`.  -/
HurwitzZeta.cosZeta_two_mul_nat' : ∀ {k : ℕ} {x : ℝ},
  k ≠ 0 →
    x ∈ Set.Icc 0 1 →
      HurwitzZeta.cosZeta (↑x) (2 * ↑k) =
        (-1) ^ (k + 1) / (2 * ↑k) / (2 * ↑k).Gammaℂ *
          Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
-- Mathlib.Tactic.GCongr.Core
/-- The name of the lemma.  -/
Mathlib.Tactic.GCongr.GCongrLemma.declName : Mathlib.Tactic.GCongr.GCongrLemma → Lean.Name
-- Mathlib.CategoryTheory.Sites.Point.Conservative
CategoryTheory.GrothendieckTopology.HasEnoughPoints.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C},
  (∃ P, CategoryTheory.ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P ∧ P.IsConservativeFamilyOfPoints) →
    J.HasEnoughPoints
-- Mathlib.SetTheory.ZFC.Class
instUnionClass : Union Class.{u_1}
-- Mathlib.Tactic.Widget.StringDiagram
Mathlib.Tactic.Widget.StringDiagram.Strand.mk.sizeOf_spec : ∀ (hPos : ℕ) (startPoint endPoint : Mathlib.Tactic.Widget.StringDiagram.Node)
  (atom₁ : Mathlib.Tactic.BicategoryLike.Atom₁),
  sizeOf { hPos := hPos, startPoint := startPoint, endPoint := endPoint, atom₁ := atom₁ } =
    1 + sizeOf hPos + sizeOf startPoint + sizeOf endPoint + sizeOf atom₁
-- Mathlib.Topology.ApproximateUnit
/-- Multiplication on the right by `m` tends to `𝓝 m` along the filter.  -/
Filter.IsApproximateUnit.tendsto_mul_right : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Mul α] {l : Filter α},
  l.IsApproximateUnit → ∀ (m : α), Filter.Tendsto (fun x => x * m) l (nhds m)
-- Mathlib.RingTheory.PolynomialLaw.Basic
/-- Tensor products in `S ⊗[R] M` can be lifted to some
`MvPolynomial R n ⊗[R] M`, for a finite `n`.  -/
PolynomialLaw.π_surjective : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type v}
  [inst_3 : CommSemiring S] [inst_4 : Algebra R S], Function.Surjective (PolynomialLaw.π R M S)
-- Mathlib.MeasureTheory.Order.Lattice
AEMeasurable.inf : ∀ {M : Type u_1} [inst : MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f g : α → M} [inst_1 : Min M] [MeasurableInf₂ M], AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (f ⊓ g) μ
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getThenInsertIfNew?.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  (m m_1 : Std.DHashMap.Raw α β),
  m = m_1 → ∀ (a : α) (b b_1 : β a), b = b_1 → m.getThenInsertIfNew? a b = m_1.getThenInsertIfNew? a b_1
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.CallHierarchy.brecOn.eq : ∀ {motive_1 : Lean.Lsp.Ipc.CallHierarchy → Sort u} {motive_2 : Array Lean.Lsp.Ipc.CallHierarchy → Sort u}
  {motive_3 : List Lean.Lsp.Ipc.CallHierarchy → Sort u} (t : Lean.Lsp.Ipc.CallHierarchy)
  (F_1 : (t : Lean.Lsp.Ipc.CallHierarchy) → t.below → motive_1 t)
  (F_2 : (t : Array Lean.Lsp.Ipc.CallHierarchy) → Lean.Lsp.Ipc.CallHierarchy.below_1 t → motive_2 t)
  (F_3 : (t : List Lean.Lsp.Ipc.CallHierarchy) → Lean.Lsp.Ipc.CallHierarchy.below_2 t → motive_3 t),
  t.brecOn F_1 F_2 F_3 = F_1 t (Lean.Lsp.Ipc.CallHierarchy.brecOn.go t F_1 F_2 F_3).2
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.whiskerLeft_app : ∀ {C D E : CategoryTheory.Cat} (F : C ⟶ D) {G H : D ⟶ E} (η : G ⟶ H) (X : ↑C),
  (CategoryTheory.Bicategory.whiskerLeft F η).toNatTrans.app X = η.toNatTrans.app (F.toFunctor.obj X)
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.SplitInclusiveIterator.instIteratorId.match_3.splitter : {ρ : Type} →
  {σ : String.Slice → Type} →
    {pat : ρ} →
      [inst : String.Slice.Pattern.ToForwardSearcher pat σ] →
        {s : String.Slice} →
          (motive : Std.IterM Id String.Slice → Sort u_1) →
            (x : Std.IterM Id String.Slice) →
              ((currPos : s.Pos) →
                  (searcher : Std.Iter (String.Slice.Pattern.SearchStep s)) →
                    motive { internalState := String.Slice.SplitInclusiveIterator.operating currPos searcher }) →
                (Unit → motive { internalState := String.Slice.SplitInclusiveIterator.atEnd }) → motive x
-- Mathlib.SetTheory.Ordinal.Veblen
/-- `veblenWith f o₁ a = veblenWith f o₂ b` iff one of the following holds:
* `o₁ = o₂` and `a = b`
* `o₁ < o₂` and `a = veblenWith f o₂ b`
* `o₁ > o₂` and `veblenWith f o₁ a = b`  -/
Ordinal.veblenWith_eq_veblenWith_iff : ∀ {f : Ordinal.{u} → Ordinal.{u}} {o₁ o₂ a b : Ordinal.{u}},
  Order.IsNormal f →
    (Ordinal.veblenWith f o₁ a = Ordinal.veblenWith f o₂ b ↔
      o₁ = o₂ ∧ a = b ∨ o₁ < o₂ ∧ a = Ordinal.veblenWith f o₂ b ∨ o₂ < o₁ ∧ Ordinal.veblenWith f o₁ a = b)
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.sum_prodMkRight : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {ι : Type u_5} [inst : Countable ι] {κ : ι → ProbabilityTheory.Kernel α β},
  (ProbabilityTheory.Kernel.sum fun i => ProbabilityTheory.Kernel.prodMkRight γ (κ i)) =
    ProbabilityTheory.Kernel.prodMkRight γ (ProbabilityTheory.Kernel.sum κ)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
Lean.Meta.Grind.Arith.Cutsat.getOfLE? : Lean.Meta.Grind.Arith.Cutsat.ToIntM (Option Lean.Expr)
-- Mathlib.Combinatorics.Matroid.Minor.Contract
/-- **Alias** of `Matroid.IsBasis'.contract_isBasis'_sdiff_sdiff_of_subset`. -/
Matroid.IsBasis'.contract_isBasis'_diff_diff_of_subset : ∀ {α : Type u_1} {M : Matroid α} {I J X : Set α}, M.IsBasis' I X → J ⊆ I → (M.contract J).IsBasis' (I \ J) (X \ J)
-- Init.Data.List.MinMaxOn
List.apply_maxOn_take_le : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {xs : List α}
  {f : α → β} {i : ℕ} (h : List.take i xs ≠ []), f (List.maxOn f (List.take i xs) h) ≤ f (List.maxOn f xs ⋯)
-- Mathlib.GroupTheory.Congruence.Basic
Con.le_iff : ∀ {M : Type u_1} [inst : MulOneClass M] {c d : Con M}, c ≤ d ↔ ↑c ≤ ↑d
-- Mathlib.Topology.Compactness.Compact
IsCompact.exists_clusterPt_of_frequently : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {l : Filter X},
  IsCompact s → (∃ᶠ (x : X) in l, x ∈ s) → ∃ a ∈ s, ClusterPt a l
-- Init.Sym.Lemmas
Lean.Sym.cond_cond_congr : ∀ {α : Sort u} (c : Bool) (a b : α) (c' : Bool), c = c' → (bif c then a else b) = bif c' then a else b
-- Mathlib.Topology.Category.Profinite.Basic
/-- The fully faithful embedding of `Profinite` in `TopCat`.
This is definitionally the same as the obvious composite.  -/
Profinite.toTopCat : CategoryTheory.Functor Profinite TopCat
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minEntry.eq_1 : ∀ {α : Type u} {β : α → Type v} (size : ℕ) (k : α) (v : β k) (r : Std.DTreeMap.Internal.Impl α β)
  (x_2 : (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).isEmpty = false),
  (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).minEntry x_2 = ⟨k, v⟩
-- Mathlib.SetTheory.ZFC.Class
Class.ext : ∀ {x y : Class.{u}}, (∀ (z : ZFSet.{u}), x z ↔ y z) → x = y
-- Lean.Util.SCC
_private.Lean.Util.SCC.0.Lean.SCC.push : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → α → Lean.SCC.M α Unit
-- Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
AlgebraicGeometry.SurjectiveOnStalks.stableUnderBaseChange : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.SurjectiveOnStalks
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ofArray.folder.match_6.congr_eq_2 : ∀ {n : ℕ} (motive : Option (Std.HashMap (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) Bool) → Sort u_1)
  (acc : Option (Std.HashMap (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) Bool)) (h_1 : Unit → motive none)
  (h_2 : (map : Std.HashMap (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) Bool) → motive (some map))
  (map : Std.HashMap (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) Bool),
  acc = some map →
    (match acc with
      | none => h_1 ()
      | some map => h_2 map) ≍
      h_2 map
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
LinearEquiv.instIsPerfPair : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M),
  (↑e).IsPerfPair
-- Mathlib.RingTheory.Ideal.Basic
Ring.exists_maximal_of_not_isField : ∀ {R : Type u_5} [inst : CommSemiring R] [Nontrivial R], ¬IsField R → ∃ p, p ≠ ⊥ ∧ p.IsMaximal
-- Init.Data.Format.Basic
/-- Creates the format `"(" ++ f ++ ")"` with a flattening group, nesting by one space.
 -/
Std.Format.paren : Std.Format → Std.Format
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.del : Lean.IR.VarId → Lean.IR.FnBody → Lean.IR.FnBody
-- Std.Async.UDP
/-- Creates a new UDP socket.
 -/
Std.Async.UDP.Socket.mk : IO Std.Async.UDP.Socket
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.precompCLM_apply : ∀ {𝕜₁ : Type u_5} {𝕜₂ : Type u_6} {𝕜₃ : Type u_7} {E : Type u_9} {F : Type u_10} {G : Type u_11} [inst : NormedField 𝕜₁]
  [inst_1 : NormedField 𝕜₂] [inst_2 : NormedField 𝕜₃] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {σ₁₃ : 𝕜₁ →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃}
  [inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_4 : AddCommGroup E] [inst_5 : TopologicalSpace E]
  [inst_6 : Module 𝕜₁ E] [inst_7 : AddCommGroup F] [inst_8 : TopologicalSpace F] [inst_9 : Module 𝕜₂ F]
  [inst_10 : AddCommGroup G] [inst_11 : TopologicalSpace G] [inst_12 : Module 𝕜₃ G] [inst_13 : IsTopologicalAddGroup G]
  [inst_14 : ContinuousConstSMul 𝕜₃ G] (f : E →SWOT[σ₁₂] F) (g : F →SWOT[σ₂₃] G), f.precompCLM g = g.comp f
-- Lean.Data.DeclarationRange
Lean.DeclarationLocation.module : Lean.DeclarationLocation → Lean.Name
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
/-- A submonoid functor consists of a submonoid of `M.obj U` for every `U`,
compatible with the restriction maps `M.map i`.  -/
CategoryTheory.SubmonoidFunctor : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor C MonCat → Type (max u w)
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.integral_eq_setToL1 : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] (f : ↥(MeasureTheory.Lp E 1 μ)),
  MeasureTheory.L1.integral f = (MeasureTheory.L1.setToL1 ⋯) f
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
TopCat.pullbackIsoProdSubtype_inv_fst_assoc : ∀ {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) {Z_1 : TopCat} (h : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (TopCat.pullbackIsoProdSubtype f g).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h) =
    CategoryTheory.CategoryStruct.comp (TopCat.pullbackFst f g) h
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cocone.toCostructuredArrowCompToOverCompForget_inv_app : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) (X : J),
  c.toCostructuredArrowCompToOverCompForget.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
-- Mathlib.Algebra.BigOperators.Finprod
/-- The sum of `f i` over `i ∈ {a, b}`, `a ≠ b`, is equal to `f a + f b`.  -/
finsum_mem_pair : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {a b : α},
  a ≠ b → ∑ᶠ (i : α) (_ : i ∈ {a, b}), f i = f a + f b
-- Init.Data.Nat.Gcd
Nat.gcd_div : ∀ {m n k : ℕ}, k ∣ m → k ∣ n → (m / k).gcd (n / k) = m.gcd n / k
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.WF.diff : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashMap.Raw α β},
  m₁.WF → m₂.WF → (m₁ \ m₂).WF
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.evalWhiskerLeft_of_cons : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {f g h i j : C}
  (α : g ≅ h) (η : h ⟶ i) {ηs : i ⟶ j}
  {θ : CategoryTheory.MonoidalCategoryStruct.tensorObj f i ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj f j},
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft f ηs = θ →
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft f
        (CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.CategoryStruct.comp η ηs)) =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeftIso f α).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft f η) θ)
-- Mathlib.Algebra.Group.Hom.Defs
AddHom.coe_mk : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (f : M → N) (hadd : ∀ (x y : M), f (x + y) = f x + f y),
  ⇑{ toFun := f, map_add' := hadd } = f
-- Mathlib.Order.Sublattice
Sublattice.map_equiv_eq_comap_symm : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (f : α ≃o β) (L : Sublattice α),
  Sublattice.map { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯ } L =
    Sublattice.comap { toFun := ⇑f.symm, map_sup' := ⋯, map_inf' := ⋯ } L
-- Mathlib.Order.SymmDiff
bihimp_himp_left : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a b : α), bihimp a b ⇨ a = a ⊔ b
-- Mathlib.Analysis.Calculus.FDeriv.Prod
HasStrictFDerivAt.fst : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {f₂ : E → F × G} {f₂' : E →L[𝕜] F × G},
  HasStrictFDerivAt f₂ f₂' x → HasStrictFDerivAt (fun x => (f₂ x).1) (ContinuousLinearMap.fst 𝕜 F G ∘SL f₂') x
-- Mathlib.Analysis.Analytic.Constructions
AnalyticAt.neg : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E},
  AnalyticAt 𝕜 f x → AnalyticAt 𝕜 (-f) x
-- Mathlib.Computability.RegularExpressions
RegularExpression.map.eq_3 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (a : α),
  RegularExpression.map f (RegularExpression.char a) = RegularExpression.char (f a)
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.toList_filterMap : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} [Std.Iterators.Finite α Id] {f : β → Option γ},
  (Std.Iter.filterMap f it).toList = List.filterMap f it.toList
-- Mathlib.CategoryTheory.Localization.Bousfield
CategoryTheory.ObjectProperty.instHasTwoOutOfThreePropertyIsColocal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C),
  P.isColocal.HasTwoOutOfThreeProperty
-- Mathlib.Algebra.Category.ModuleCat.ExteriorPower
ModuleCat.exteriorPower.hom_ext_iff : ∀ {R : Type u} [inst : CommRing R] {M : ModuleCat R} {N : ModuleCat R} {n : ℕ} {f g : M.exteriorPower n ⟶ N},
  f = g ↔ ModuleCat.exteriorPower.mk.postcomp f = ModuleCat.exteriorPower.mk.postcomp g
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.aroots.eq_1 : ∀ {T : Type w} [inst : CommRing T] (p : Polynomial T) (S : Type u_1) [inst_1 : CommRing S] [inst_2 : IsDomain S]
  [inst_3 : Algebra T S], p.aroots S = (Polynomial.map (algebraMap T S) p).roots