mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.leftInvSeq.eq_def : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B),
  cs.leftInvSeq ω =
    match ω with
    | [] => []
    | i :: ω => cs.simple i :: List.map (⇑(MulAut.conj (cs.simple i))) (cs.leftInvSeq ω)
-- Mathlib.Algebra.Algebra.Unitization
/-- `starMap` is functorial: `starMap (ψ.comp φ) = (starMap ψ).comp (starMap φ)`.  -/
Unitization.starMap_comp : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : NonUnitalSemiring A] [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : SMulCommClass R A A]
  [inst_6 : IsScalarTower R A A] [inst_7 : NonUnitalSemiring B] [inst_8 : StarRing B] [inst_9 : Module R B]
  [inst_10 : SMulCommClass R B B] [inst_11 : IsScalarTower R B B] [inst_12 : NonUnitalSemiring C] [inst_13 : StarRing C]
  [inst_14 : Module R C] [inst_15 : SMulCommClass R C C] [inst_16 : IsScalarTower R C C] [inst_17 : StarModule R B]
  [inst_18 : StarModule R C] {φ : A →⋆ₙₐ[R] B} {ψ : B →⋆ₙₐ[R] C},
  Unitization.starMap (ψ.comp φ) = (Unitization.starMap ψ).comp (Unitization.starMap φ)
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- Let `M₁ᵢ` and `M₁ᵢ'` be two families of `R`-modules and `M₂` an `R`-module.
Let us denote `Π i, M₁ᵢ` and `Π i, M₁ᵢ'` by `M` and `M'` respectively.
If `g` is a multilinear map `M' → M₂`, then `g` can be reinterpreted as a multilinear
map from `Π i, M₁ᵢ ⟶ M₁ᵢ'` to `M ⟶ M₂` via `(fᵢ) ↦ v ↦ g(fᵢ vᵢ)`.
 -/
MultilinearMap.piLinearMap : {R : Type uR} →
  {ι : Type uι} →
    {M₁ : ι → Type v₁} →
      {M₁' : ι → Type v₁'} →
        {M₂ : Type v₂} →
          [inst : CommSemiring R] →
            [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
              [inst_2 : AddCommMonoid M₂] →
                [inst_3 : (i : ι) → Module R (M₁ i)] →
                  [inst_4 : Module R M₂] →
                    [inst_5 : (i : ι) → AddCommMonoid (M₁' i)] →
                      [inst_6 : (i : ι) → Module R (M₁' i)] →
                        MultilinearMap R M₁' M₂ →ₗ[R]
                          MultilinearMap R (fun i => M₁ i →ₗ[R] M₁' i) (MultilinearMap R M₁ M₂)
-- Init.Data.SInt.Bitwise
Int16.toUInt16_xor : ∀ (a b : Int16), (a ^^^ b).toUInt16 = a.toUInt16 ^^^ b.toUInt16
-- Mathlib.Topology.Order.Hom.Basic
ContinuousOrderHom.instFunLike : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : Preorder α] → [inst_2 : TopologicalSpace β] → [inst_3 : Preorder β] → FunLike (α →Co β) α β
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.size_le_size_alter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : LawfulBEq α] {k : α} {f : Option β → Option β},
  m.WF → m.size - 1 ≤ (Std.DHashMap.Raw.Const.alter m k f).size
-- Mathlib.Geometry.Manifold.Algebra.SMul
instContMDiffSMulOfSomeENatTopOfLEInfty : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {G : Type u_8} [inst_7 : TopologicalSpace G] [inst_8 : ChartedSpace H G]
  {M : Type u_9} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H' M] [inst_11 : SMul G M] {n : WithTop ℕ∞}
  [ContMDiffSMul I I' (↑⊤) G M] [ENat.LEInfty n], ContMDiffSMul I I' n G M
-- Mathlib.RingTheory.Ideal.GoingUp
Ideal.coeff_zero_mem_comap_of_root_mem_of_eval_mem : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {f : R →+* S} {I : Ideal S} {r : S},
  r ∈ I → ∀ {p : Polynomial R}, Polynomial.eval₂ f r p ∈ I → p.coeff 0 ∈ Ideal.comap f I
-- Init.Data.Int.DivMod.Lemmas
Int.lt_mul_of_tdiv_lt : ∀ {a b c : ℤ}, 0 < c → a.tdiv c < b → a < b * c
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.vlt_of_veq_of_vlt : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y z : R}, x =ᵥ y → y <ᵥ z → x <ᵥ z
-- Mathlib.Data.Sum.Interval
Sum.Lex.Icc_inr_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] [inst_4 : LocallyFiniteOrderTop α] [inst_5 : LocallyFiniteOrderBot β] (a : α) (b : β),
  Finset.Icc (Sum.inrₗ b) (Sum.inlₗ a) = ∅
-- Mathlib.Algebra.BigOperators.Finprod
/-- A more general version of `finprod_mem_insert` that requires `s ∩ mulSupport f` rather than `s`
to be finite.  -/
finprod_mem_insert' : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {a : α} {s : Set α} (f : α → M),
  a ∉ s → (s ∩ Function.mulSupport f).Finite → ∏ᶠ (i : α) (_ : i ∈ insert a s), f i = f a * ∏ᶠ (i : α) (_ : i ∈ s), f i
-- Mathlib.Algebra.Category.MonCat.ForgetCorepresentable
/-- Monoid homomorphisms from `ULift (Multiplicative ℕ)` are defined by the image
of `Multiplicative.ofAdd 1`.  -/
uliftPowersHom : (M : Type u) → [inst : Monoid M] → M ≃ (ULift.{u, 0} (Multiplicative ℕ) →* M)
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The lifted cocone on `Under X` is a colimit cocone if the original cocone was colimiting
and `J` is nonempty.  -/
CategoryTheory.Under.isColimitLiftCocone : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {J : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} J] →
        [Nonempty J] →
          (D : CategoryTheory.Functor J T) →
            {X : T} →
              (s : (CategoryTheory.Functor.const J).obj X ⟶ D) →
                (c : CategoryTheory.Limits.Cocone D) →
                  (p : X ⟶ c.pt) →
                    (hp : ∀ (j : J), CategoryTheory.CategoryStruct.comp (s.app j) (c.ι.app j) = p) →
                      CategoryTheory.Limits.IsColimit c →
                        CategoryTheory.Limits.IsColimit (CategoryTheory.Under.liftCocone D s c p hp)
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.weightedTotalDegree'.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : SemilatticeSup M] (w : σ → M) (p : MvPolynomial σ R),
  MvPolynomial.weightedTotalDegree' w p = p.support.sup fun s => ↑((Finsupp.weight w) s)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.OneHypercover.comp_h₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {S : C}
  {X Y Z : J.OneHypercover S} (f : X.Hom Y) (g : Y.Hom Z) {i j : X.I₀} (i_1 : X.I₁ i j),
  (CategoryTheory.CategoryStruct.comp f g).h₁ i_1 = CategoryTheory.CategoryStruct.comp (f.h₁ i_1) (g.h₁ (f.s₁ i_1))
-- Mathlib.NumberTheory.PrimeCounting
/-- A variant of the traditional prime counting function which gives the number of primes
*strictly* less than the input. More convenient for avoiding off-by-one errors.

With `open scoped Nat.Prime`, this has notation `π'`.  -/
Nat.primeCounting' : ℕ → ℕ
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.induction_on₃ : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  {α' : Type u_5} {β' : Type u_6} [inst_2 : MeasurableSpace α'] [inst_3 : TopologicalSpace β']
  {μ' : MeasureTheory.Measure α'} {α'' : Type u_7} {β'' : Type u_8} [inst_4 : MeasurableSpace α'']
  [inst_5 : TopologicalSpace β''] {μ'' : MeasureTheory.Measure α''} (f : α →ₘ[μ] β) (f' : α' →ₘ[μ'] β')
  (f'' : α'' →ₘ[μ''] β'') {p : (α →ₘ[μ] β) → (α' →ₘ[μ'] β') → (α'' →ₘ[μ''] β'') → Prop},
  (∀ (f : α → β) (hf : MeasureTheory.AEStronglyMeasurable f μ) (f' : α' → β')
      (hf' : MeasureTheory.AEStronglyMeasurable f' μ') (f'' : α'' → β'')
      (hf'' : MeasureTheory.AEStronglyMeasurable f'' μ''),
      p (MeasureTheory.AEEqFun.mk f hf) (MeasureTheory.AEEqFun.mk f' hf') (MeasureTheory.AEEqFun.mk f'' hf'')) →
    p f f' f''
-- Mathlib.Order.Interval.Set.Pi
Set.image_mulSingle_uIcc : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Lattice (α i)] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → One (α i)] (i : ι) (a b : α i),
  Pi.mulSingle i '' Set.uIcc a b = Set.uIcc (Pi.mulSingle i a) (Pi.mulSingle i b)
-- Mathlib.Topology.Compactness.CountablyCompact
isSeqCompact_univ_iff : ∀ {E : Type u_2} [inst : TopologicalSpace E], IsSeqCompact Set.univ ↔ SeqCompactSpace E
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The underlying lean expression of a 2-isomorphism.  -/
Mathlib.Tactic.BicategoryLike.Mor₂Iso.e : Mathlib.Tactic.BicategoryLike.Mor₂Iso → Lean.Expr
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.measurableSet_generateFrom_memPartition : ∀ {α : Type u_1} (t : ℕ → Set α) (n : ℕ), MeasurableSet (t n)
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupNorm.toGroupSeminorm : {G : Type u_6} → [inst : Group G] → GroupNorm G → GroupSeminorm G
-- Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
CategoryTheory.MorphismProperty.IsInvertedBy.pi : ∀ {J : Type w} {C : J → Type u} {D : J → Type u'} [inst : (j : J) → CategoryTheory.Category.{v, u} (C j)]
  [inst_1 : (j : J) → CategoryTheory.Category.{v', u'} (D j)] (W : (j : J) → CategoryTheory.MorphismProperty (C j))
  (F : (j : J) → CategoryTheory.Functor (C j) (D j)),
  (∀ (j : J), (W j).IsInvertedBy (F j)) →
    (CategoryTheory.MorphismProperty.pi W).IsInvertedBy (CategoryTheory.Functor.pi F)
-- Mathlib.RingTheory.TensorProduct.Basic
LinearMap.mulLeft_tmul : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : SMulCommClass R A A]
  [inst_6 : SMulCommClass R B B] [inst_7 : IsScalarTower R A A] [inst_8 : IsScalarTower R B B] (a : A) (b : B),
  LinearMap.mulLeft R (a ⊗ₜ[R] b) = TensorProduct.map (LinearMap.mulLeft R a) (LinearMap.mulLeft R b)
-- Init.Data.Int.Order
Int.negSucc_le_zero : ∀ (n : ℕ), Int.negSucc n ≤ 0
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.eventually_r_pos : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), 0 < r i n
-- Mathlib.Data.Set.Prod
/-- **Alias** of `Set.prod_mono_left`. -/
Set.prod_subset_prod_left : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t : Set β}, s₁ ⊆ s₂ → s₁ ×ˢ t ⊆ s₂ ×ˢ t
-- Mathlib.Algebra.Group.Ideal
AddSemigroupIdeal.eq_1 : ∀ (M : Type u_1) [inst : Add M], AddSemigroupIdeal M = SubAddAction M M
-- Mathlib.RingTheory.Nakayama
Submodule.le_of_map_mkQ_le_map_mkQ_of_le_jacobson_bot : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  {N N' : Submodule R M}, N.FG → I ≤ ⊥.jacobson → Submodule.map (I • N).mkQ N ≤ Submodule.map (I • N).mkQ N' → N ≤ N'
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.leftQuotientEquiv.eq_1 : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {S : Set G} (hS : Subgroup.IsComplement S ↑H),
  hS.leftQuotientEquiv = (Equiv.ofBijective (S.domRestrict QuotientGroup.mk) ⋯).symm
-- Lean.Widget.UserWidget
Lean.Widget.addPanelWidgetGlobal : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → [Lean.MonadResolveName m] → UInt64 → Lean.Name → m Unit
-- Mathlib.Tactic.ClickSuggestions
/-- Run `k` with the `RwKind` of the selected position, and the subexpression at that position.
If the subexpression contains bound variables, then they are introduced as free variables.  -/
_private.Mathlib.Tactic.ClickSuggestions.0.Mathlib.Tactic.ClickSuggestions.viewKAbstractSubExpr' : {m : Type → Type} →
  {α : Type} →
    [Monad m] →
      [MonadLiftT Lean.MetaM m] →
        [MonadControlT Lean.MetaM m] →
          [Lean.MonadError m] →
            Lean.Expr → Lean.SubExpr.Pos → (Lean.Expr → Mathlib.Tactic.ClickSuggestions.RwKind → m α) → m α
-- Init.Data.String.Lemmas.Intercalate
_private.Init.Data.String.Lemmas.Intercalate.0.String.Slice.intercalate.match_1.splitter : (motive : List String.Slice → Sort u_1) →
  (x : List String.Slice) →
    (Unit → motive []) → ((a : String.Slice) → (as : List String.Slice) → motive (a :: as)) → motive x
-- Mathlib.Algebra.SkewMonoidAlgebra.Single
SkewMonoidAlgebra.coeff_update_apply : ∀ {M : Type u_4} {α : Type u_5} [inst : AddCommMonoid M] (f : SkewMonoidAlgebra M α) (a a' : α) (b : M)
  [inst_1 : DecidableEq α], (f.update a b).coeff a' = if a' = a then b else f.coeff a'
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.eventually : ∀ {α : Type u} {β : Type v} {l : Filter α} {f g : α → β}, f =ᶠ[l] g → ∀ᶠ (x : α) in l, f x = g x
-- Mathlib.NumberTheory.Dioph
Fin2.ofNat'.congr_simp : ∀ {n : ℕ} (m m_1 : ℕ) (e_m : m = m_1) [inst : Fin2.IsLT m n], Fin2.ofNat' m = Fin2.ofNat' m_1
-- Mathlib.CategoryTheory.Bicategory.Opposites
/-- A 2-isomorphism in `B` gives a 2-isomorphism in `Bᵒᵖ`  -/
CategoryTheory.Iso.op2 : {B : Type u} → [inst : CategoryTheory.Bicategory B] → {a b : B} → {f g : a ⟶ b} → (f ≅ g) → (f.op ≅ g.op)
-- Mathlib.Order.Heyting.Hom
HeytingHom.mk.sizeOf_spec : ∀ {α : Type u_6} {β : Type u_7} [inst : HeytingAlgebra α] [inst_1 : HeytingAlgebra β] [inst_2 : SizeOf α]
  [inst_3 : SizeOf β] (toLatticeHom : LatticeHom α β) (map_bot' : toLatticeHom.toFun ⊥ = ⊥)
  (map_himp' : ∀ (a b : α), toLatticeHom.toFun (a ⇨ b) = toLatticeHom.toFun a ⇨ toLatticeHom.toFun b),
  sizeOf { toLatticeHom := toLatticeHom, map_bot' := map_bot', map_himp' := map_himp' } =
    1 + sizeOf toLatticeHom + sizeOf map_bot'
-- Mathlib.Data.Set.Image
Set.disjoint_image_image : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β → α} {g : γ → α} {s : Set β} {t : Set γ},
  (∀ b ∈ s, ∀ c ∈ t, f b ≠ g c) → Disjoint (f '' s) (g '' t)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mdifferentiableWithinAt_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {s : Set M} {x : M} {c : M'},
  (MDiffAt[s] fun x => c) x
-- Mathlib.CategoryTheory.Limits.Types.Products
CategoryTheory.Limits.Types.productIso_inv_comp_π : ∀ {J : Type v} (F : J → Type (max v u)) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.productIso F).inv (CategoryTheory.Limits.Pi.π F j) =
    TypeCat.ofHom fun f => f j
-- Mathlib.Order.Disjoint
/-- Two elements of a lattice are codisjoint if their sup is the top element.

Note that we define this without reference to `⊔`, as this allows us to talk about orders where
the supremum is not unique, or where implementing `Sup` would require additional `Decidable`
arguments.  -/
Codisjoint : {α : Type u_1} → [inst : PartialOrder α] → [OrderTop α] → α → α → Prop
-- Lean.Data.Lsp.Basic
Lean.Lsp.PartialResultParams.mk.injEq : ∀ (partialResultToken? partialResultToken?_1 : Option Lean.Lsp.ProgressToken),
  ({ partialResultToken? := partialResultToken? } = { partialResultToken? := partialResultToken?_1 }) =
    (partialResultToken? = partialResultToken?_1)
-- Mathlib.Algebra.BigOperators.WithTop
/-- A sum is infinite iff one term is infinite.  -/
WithBot.sum_eq_bot_iff : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {s : Finset ι} {f : ι → WithBot M},
  ∑ i ∈ s, f i = ⊥ ↔ ∃ i ∈ s, f i = ⊥
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionHomLeft : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {d d' : C} (f : d ⟶ d') (c : CategoryTheory.Functor C C),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f c = c.map f
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k fallback : α}, k ∉ m₂ → (m₁ ∪ m₂).getKeyD k fallback = m₁.getKeyD k fallback
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemTag.noConfusionType : Sort v✝ → Lean.Lsp.CompletionItemTag → Lean.Lsp.CompletionItemTag → Sort v✝
-- Mathlib.GroupTheory.Subgroup.Simple
isSimpleGroup_iff : ∀ (G : Type u_1) [inst : Group G], IsSimpleGroup G ↔ Nontrivial G ∧ ∀ (H : Subgroup G), H.Normal → H = ⊥ ∨ H = ⊤
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.contradiction_of_insertUnit_fold_success : ∀ {n : ℕ} (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (assignments_size : assignments.size = n)
  (units : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) (foundContradiction : Bool)
  (l : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  let insertUnit_fold_res :=
    List.foldl Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit (units, assignments, foundContradiction) l;
  (foundContradiction = true → ∃ i, assignments[↑i] = Std.Tactic.BVDecide.LRAT.Internal.Assignment.both) →
    insertUnit_fold_res.2.2 = true →
      ∃ j, insertUnit_fold_res.2.1[↑j] = Std.Tactic.BVDecide.LRAT.Internal.Assignment.both
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.support.congr_simp : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  {inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)} [inst_3 : (i : ι) → (x : β i) → Decidable (x ≠ 0)]
  (f f_1 : Π₀ (i : ι), β i), f = f_1 → f.support = f_1.support
-- Mathlib.GroupTheory.Subgroup.Center
/-- The center of a group is isomorphic to the center of its opposite.  -/
Subgroup.centerToMulOpposite : (G : Type u_1) → [inst : Group G] → ↥(Subgroup.center G) ≃* ↥(Subgroup.center Gᵐᵒᵖ)
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.OuterRegular.mk : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] {μ : MeasureTheory.Measure α},
  (∀ ⦃A : Set α⦄, MeasurableSet A → ∀ r > μ A, ∃ U ⊇ A, IsOpen U ∧ μ U < r) → μ.OuterRegular
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.instMonoidalInverseSymmOfFunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] → (e : C ≌ D) → [e.functor.Monoidal] → e.symm.inverse.Monoidal
-- Mathlib.ModelTheory.Basic
/-- Composition of first-order embeddings.  -/
FirstOrder.Language.Embedding.comp : {L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type w'} →
      [inst : L.Structure M] →
        [inst_1 : L.Structure N] →
          {P : Type u_1} → [inst_2 : L.Structure P] → L.Embedding N P → L.Embedding M N → L.Embedding M P
-- Lean.Meta.Match.AltTelescopes
/-- Similar to `forallTelescopeReducing`, but

1. Eliminates arguments for named parameters and the associated equation proofs.

2. Instantiate the `Unit` parameter of an otherwise argumentless alternative.

It does not handle the equality parameters associated with the `h : discr` notation.

The continuation `k` takes four arguments `ys args mask type`.
- `ys` are variables for the hypotheses that have not been eliminated.
- `args` are the arguments for the alternative `alt` that has type `altType`. `ys.size <= args.size`
- `mask[i]` is true if the hypotheses has not been eliminated. `mask.size == args.size`.
- `type` is the resulting type for `altType`.

We use the `mask` to build the splitter proof. See `mkSplitterProof`.

This can be used to use the alternative of a match expression in its splitter.
 -/
Lean.Meta.Match.forallAltVarsTelescope : {α : Type} →
  Lean.Expr →
    Lean.Meta.Match.AltParamInfo →
      (Array Lean.Expr → Array Lean.Expr → Array Bool → Lean.Expr → Lean.MetaM α) → Lean.MetaM α
-- Init.WFComputable
Acc.ndrecC.eq_1 : ∀ {α : Sort u_1} {r : α → α → Prop} {C : α → Sort v}
  (m : (x : α) → (∀ (y : α), r y x → Acc r y) → ((y : α) → r y x → C y) → C x) {a : α} (n : Acc r a),
  Acc.ndrecC m n = Acc.recC m n
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLTLTToLT_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : EInt) (X : C),
  (t.eTruncLTLTToLT a b).app X = (t.eTruncLT.obj b).map ((t.eTruncLTι a).app X)
-- Init.Data.UInt.IntToBitVec
USize.eq_iff_toBitVec32_eq : ∀ {a b : USize} (h : System.Platform.numBits = 32), a = b ↔ a.toBitVec32 h = b.toBitVec32 h
-- Mathlib.NumberTheory.Pell
/-- The `y`-coordinate of a fundamental solution is a lower bound for the `y`-coordinate
of any positive solution.  -/
Pell.IsFundamental.y_le_y : ∀ {d : ℤ} {a₁ : Pell.Solution₁ d}, Pell.IsFundamental a₁ → ∀ {a : Pell.Solution₁ d}, 1 < a.x → 0 < a.y → a₁.y ≤ a.y
-- Mathlib.RingTheory.Algebraic.Basic
/-- In an algebraic extension L/K, an intermediate subalgebra is a field.  -/
Subalgebra.isField_of_algebraic : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (A : Subalgebra K L)
  [Algebra.IsAlgebraic K L], IsField ↥A
-- Mathlib.Algebra.Lie.Normalizer
/-- The idealizer of a Lie submodule.

See also `LieSubmodule.normalizer`.  -/
LieSubmodule.idealizer : {R : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] → [LieModule R L M] → LieSubmodule R L M → LieIdeal R L
-- Mathlib.Data.Multiset.Antidiagonal
Multiset.antidiagonal_coe' : ∀ {α : Type u_1} (l : List α), (↑l).antidiagonal = ↑(Multiset.powersetAux' l).revzip
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Group.nilpotencyClass_pi`.

---

The nilpotency class of an n-ary product is the sup of the nilpotency classes of the factors.  -/
nilpotencyClass_pi : ∀ {η : Type u_2} {Gs : η → Type u_3} [inst : (i : η) → Group (Gs i)] [inst_1 : Fintype η]
  [∀ (i : η), Group.IsNilpotent (Gs i)],
  Group.nilpotencyClass ((i : η) → Gs i) = Finset.univ.sup fun i => Group.nilpotencyClass (Gs i)
-- Mathlib.Algebra.Free
FreeMagma.mul_bind : ∀ {α β : Type u} (f : α → FreeMagma β) (x y : FreeMagma α), x * y >>= f = (x >>= f) * (y >>= f)
-- Mathlib.Data.Finset.Sym
Finset.sym2_eq_empty : ∀ {α : Type u_1} {s : Finset α}, s.sym2 = ∅ ↔ s = ∅
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearEquiv.rTensor_trans_apply : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10}
  [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] (g : P ≃ₗ[R] Q)
  (f : N ≃ₗ[R] P) (y : TensorProduct R N M),
  (LinearEquiv.rTensor M (f ≪≫ₗ g)) y = (LinearEquiv.rTensor M g) ((LinearEquiv.rTensor M f) y)
-- Mathlib.Algebra.Order.Group.PosPart
Pi.leOnePart_apply : ∀ {ι : Type u_2} {α : ι → Type u_3} [inst : (i : ι) → Lattice (α i)] [inst_1 : (i : ι) → Group (α i)]
  (f : (i : ι) → α i) (i : ι), f⁻ᵐ i = (f i)⁻ᵐ
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- The product of a function `g` defined only on a set `s` is equal to
the product of a function `f` defined everywhere,
as long as `f` and `g` agree on `s`, and `f = 1` off `s`.  -/
Finset.prod_congr_set : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] [inst_1 : Fintype ι] (s : Set ι)
  [inst_2 : DecidablePred fun x => x ∈ s] (f : ι → M) (g : ↑s → M),
  (∀ (x : ι) (hx : x ∈ s), f x = g ⟨x, hx⟩) → (∀ x ∉ s, f x = 1) → ∏ i, f i = ∏ i, g i