mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.ITauto
/-- The main prover. This receives a context of proven or assumed lemmas and a target proposition,
and returns a proof or `none` (with state for the fresh variable generator).
The intuitionistic logic rules are separated into three groups:

* level 1: No splitting, validity preserving: apply whenever you can.
  Left rules in `Context.add`, right rules in `prove`
* level 2: Splitting rules, validity preserving: apply after level 1 rules. Done in `prove`
* level 3: Splitting rules, not validity preserving: apply only if nothing else applies.
  Done in `search`

The level 1 rules on the right of the turnstile are `Γ ⊢ ⊤` and `Γ ⊢ A → B`, these are easy to
handle. The rule `Γ ⊢ A ∧ B` is a level 2 rule, also handled here. If none of these apply, we try
the level 2 rule `A ∨ B ⊢ C` by searching the context and splitting all ors we find. Finally, if
we don't make any more progress, we go to the search phase.
 -/
Mathlib.Tactic.ITauto.prove : Mathlib.Tactic.ITauto.Context → Mathlib.Tactic.ITauto.IProp → StateM ℕ (Bool × Mathlib.Tactic.ITauto.Proof)
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.liftPropWithinAt_self_target : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M]
  [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H'] {P : (H → H') → Set H → H → Prop} {s : Set M} {x : M}
  {f : M → H'},
  ChartedSpace.LiftPropWithinAt P f s x ↔
    ContinuousWithinAt f s x ∧ P (f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x)
-- Mathlib.LinearAlgebra.BilinearForm.Hom
LinearMap.BilinForm.congr_comp : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type u_7}
  {M'' : Type u_8} [inst_3 : AddCommMonoid M'] [inst_4 : AddCommMonoid M''] [inst_5 : Module R M']
  [inst_6 : Module R M''] (e : M ≃ₗ[R] M') (B : LinearMap.BilinForm R M) (l r : M'' →ₗ[R] M'),
  ((LinearMap.BilinForm.congr e) B).comp l r = B.comp (↑e.symm ∘ₗ l) (↑e.symm ∘ₗ r)
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.instIsIsoHom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {A B : CategoryTheory.Pretriangulated.Triangle C} (φ : A ⟶ B) [CategoryTheory.IsIso φ], CategoryTheory.IsIso φ.hom₃
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_modify : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF →
    ∀ {k k' fallback : α} {f : β k → β k},
      (m.modify k f).getKeyD k' fallback =
        if (k == k') = true then if m.contains k = true then k else fallback else m.getKeyD k' fallback
-- Mathlib.Algebra.Group.Pi.Basic
Sum.elim_sub_sub : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a a' : α → γ) (b b' : β → γ) [inst : Sub γ],
  Sum.elim (a - a') (b - b') = Sum.elim a b - Sum.elim a' b'
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctorStruct.mk : {B : Type u₁} →
  [inst : Quiver B] →
    [inst_1 : (a b : B) → Quiver (a ⟶ b)] →
      {C : Type u₂} →
        [inst_2 : Quiver C] →
          [inst_3 : (a b : C) → Quiver (a ⟶ b)] →
            (toPrefunctor : B ⥤q C) →
              ({a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (toPrefunctor.map f ⟶ toPrefunctor.map g)) →
                CategoryTheory.PrelaxFunctorStruct B C
-- Init.Data.Array.Erase
Array.erase_eq_eraseIdx_of_idxOf : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {xs : Array α} {a : α} {i : ℕ},
  Array.idxOf a xs = i → ∀ (h : i < xs.size), xs.erase a = xs.eraseIdx i h
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.toList_zero : ∀ {α : Type u_1}, FreeAddMonoid.toList 0 = []
-- Init.Data.Range.Polymorphic.UInt
UInt64.instLawfulHasSize : Std.Rxc.LawfulHasSize UInt64
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.coordinate.eq_1 : ∀ (i : ℕ), Lean.Omega.LinearCombo.coordinate i = { coeffs := Lean.Omega.Coeffs.set [] i 1 }
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.φ_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z) {Z_1 : C} (h : CategoryTheory.Limits.cokernel (CategoryTheory.CategoryStruct.comp f g) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.kernelCokernelCompSequence.φ f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.kernelCokernelCompSequence.π f g) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- Calculate the integral of `(g ∘ f)`, where `g : β → ℝ≥0∞` and `f : α →ₛ β`.  -/
MeasureTheory.SimpleFunc.map_lintegral : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (g : β → ENNReal)
  (f : MeasureTheory.SimpleFunc α β),
  (MeasureTheory.SimpleFunc.map g f).lintegral μ = ∑ x ∈ f.range, g x * μ (⇑f ⁻¹' {x})
-- Mathlib.Probability.Distributions.Gaussian.Basic
ProbabilityTheory.isGaussian_of_isGaussian_map : ∀ {E : Type u_1} [inst : TopologicalSpace E] [inst_1 : AddCommMonoid E] [inst_2 : Module ℝ E] {mE : MeasurableSpace E}
  [OpensMeasurableSpace E] {μ : MeasureTheory.Measure E},
  (∀ (L : E →L[ℝ] ℝ), ProbabilityTheory.IsGaussian (MeasureTheory.Measure.map (⇑L) μ)) → ProbabilityTheory.IsGaussian μ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.class.sizeOf_spec : sizeOf Lean.Lsp.SymbolKind.class = 1
-- Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence
AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyHomInvId : ∀ {A : Type u_2} [inst : CategoryTheory.Category.{v_2, u_2} A] [inst_1 : CategoryTheory.Abelian A]
  {Y : CategoryTheory.SimplicialObject A},
  AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex.homotopyHomInvId =
    Homotopy.ofEq ⋯
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
/-- This is not listed as an instance because we often want to replace the topology, uniformity
and bornology instead of inheriting them from the norm.  -/
CStarModule.normedAddCommGroup : (A : Type u_1) →
  {E : Type u_2} →
    [inst : NonUnitalCStarAlgebra A] →
      [inst_1 : PartialOrder A] →
        [inst_2 : AddCommGroup E] →
          [inst_3 : Module ℂ E] →
            [inst_4 : SMul A E] → [inst_5 : Norm E] → [CStarModule A E] → [StarOrderedRing A] → NormedAddCommGroup E
-- Mathlib.AlgebraicGeometry.Morphisms.LocalIso
AlgebraicGeometry.IsLocalIso.eq_sourceLocalClosure_isOpenImmersion : @AlgebraicGeometry.IsLocalIso =
  AlgebraicGeometry.sourceLocalClosure AlgebraicGeometry.IsOpenImmersion AlgebraicGeometry.IsOpenImmersion
-- Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
PointwiseConvergenceCLM.postcomp_apply : ∀ {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} {𝕜₃ : Type u_6} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂]
  [inst_2 : NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [inst_3 : RingHomCompTriple σ τ ρ]
  (E : Type u_7) {F : Type u_8} {G : Type u_10} [inst_4 : AddCommGroup E] [inst_5 : TopologicalSpace E]
  [inst_6 : AddCommGroup F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F] [inst_9 : AddCommGroup G]
  [inst_10 : TopologicalSpace G] [inst_11 : IsTopologicalAddGroup G] [inst_12 : Module 𝕜₁ E] [inst_13 : Module 𝕜₂ F]
  [inst_14 : Module 𝕜₃ G] [inst_15 : ContinuousConstSMul 𝕜₂ F] [inst_16 : ContinuousConstSMul 𝕜₃ G] (L : F →SL[τ] G)
  (f : E →SLₚₜ[σ] F), (PointwiseConvergenceCLM.postcomp E L) f = L ∘SL f
-- Mathlib.Topology.Algebra.Module.Star
symm_starL' : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : AddCommMonoid A]
  [inst_3 : StarAddMonoid A] [inst_4 : Module R A] [inst_5 : StarModule R A] [inst_6 : TopologicalSpace A]
  [inst_7 : ContinuousStar A] [inst_8 : TrivialStar R], (starL' R).symm = starL' R
-- Init.WFComputable
Acc.ndrecOn.eq_1 : ∀ {α : Sort u2} {r : α → α → Prop} {C : α → Sort u1} {a : α} (n : Acc r a)
  (m : (x : α) → (∀ (y : α), r y x → Acc r y) → ((y : α) → r y x → C y) → C x), n.ndrecOn m = Acc.rec m n
-- Mathlib.Topology.EMetricSpace.Defs
/-- EMetric space instance on subsets of emetric spaces  -/
instEMetricSpaceSubtype : {α : Type u_2} → {p : α → Prop} → [EMetricSpace α] → EMetricSpace (Subtype p)
-- Mathlib.Data.Sym.Sym2.Finsupp
Finsupp.support_sym2Mul_subset : ∀ {α : Type u_1} {M₀ : Type u_2} [inst : CommMonoidWithZero M₀] {f : α →₀ M₀}, f.sym2Mul.support ⊆ f.support.sym2
-- Mathlib.Computability.RegularExpressions
RegularExpression.one_rmatch_iff : ∀ {α : Type u_1} [inst : DecidableEq α] (x : List α), RegularExpression.rmatch 1 x = true ↔ x = []
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_leftUnitor : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} B₁]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁}
  (X : Type u₇) [inst_6 : CategoryTheory.Category.{v₇, u₇} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁),
  (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).map ψ.leftUnitor.hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp X
          (CategoryTheory.Limits.CatCospanTransform.id F G) ψ).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight
          (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId X F G).hom
          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ))
        ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).leftUnitor.hom)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.congrLeft_unitIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D) (X : CategoryTheory.Functor C E),
  e.congrLeft.unitIso.hom.app X = (e.funInvIdAssoc X).inv
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.insert.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (v : β k) (t : Std.DTreeMap.Internal.Impl α β) (hl : t.Balanced),
  Std.DTreeMap.Internal.Impl.insert k v t hl =
    match t, hl with
    | Std.DTreeMap.Internal.Impl.leaf, hl =>
      { impl := Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf,
        balanced_impl := ⋯, lb_le_size_impl := ⋯, size_impl_le_ub := ⋯ }
    | Std.DTreeMap.Internal.Impl.inner sz k' v' l' r', hl =>
      match compare k k' with
      | Ordering.lt =>
        match Std.DTreeMap.Internal.Impl.insert k v l' ⋯ with
        | { impl := d, balanced_impl := hd, lb_le_size_impl := hd₁, size_impl_le_ub := hd₂ } =>
          { impl := Std.DTreeMap.Internal.Impl.balanceL k' v' d r' ⋯ ⋯ ⋯, balanced_impl := ⋯, lb_le_size_impl := ⋯,
            size_impl_le_ub := ⋯ }
      | Ordering.gt =>
        match Std.DTreeMap.Internal.Impl.insert k v r' ⋯ with
        | { impl := d, balanced_impl := hd, lb_le_size_impl := hd₁, size_impl_le_ub := hd₂ } =>
          { impl := Std.DTreeMap.Internal.Impl.balanceR k' v' l' d ⋯ ⋯ ⋯, balanced_impl := ⋯, lb_le_size_impl := ⋯,
            size_impl_le_ub := ⋯ }
      | Ordering.eq =>
        { impl := Std.DTreeMap.Internal.Impl.inner sz k v l' r', balanced_impl := ⋯, lb_le_size_impl := ⋯,
          size_impl_le_ub := ⋯ }
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.union.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (t₁ t₂ : Std.DTreeMap.Internal.Impl α β) (h₁ : t₁.Balanced)
  (h₂ : t₂.Balanced),
  t₁.union t₂ h₁ h₂ = if t₁.size ≤ t₂.size then ↑(t₂.insertManyIfNew t₁ h₂) else ↑(t₁.insertMany t₂ h₁)
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.range_eq_univ : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂), Set.range ⇑e = Set.univ
-- Mathlib.Algebra.Order.Rearrangement
/-- **Rearrangement Inequality**: Pointwise scalar multiplication of `f` and `g` is maximized when
`f` and `g` monovary together on `s`. Stated by permuting the entries of `f`.  -/
MonovaryOn.sum_comp_perm_smul_le_sum_smul : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [ExistsAddOfLE α] [inst_4 : AddCommMonoid β] [inst_5 : LinearOrder β] [IsOrderedCancelAddMonoid β]
  [inst_7 : Module α β] [PosSMulMono α β] {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
-- Mathlib.Topology.Order.IntermediateValue
/-- Intermediate value theorem for two functions: if `f` and `g` are two continuous functions
on a preconnected space and `f a ≤ g a` and `g b ≤ f b`, then for some `x` we have `f x = g x`.  -/
intermediate_value_univ₂ : ∀ {X : Type u} {α : Type v} [inst : TopologicalSpace X] [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α]
  [OrderClosedTopology α] [PreconnectedSpace X] {a b : X} {f g : X → α},
  Continuous f → Continuous g → f a ≤ g a → g b ≤ f b → ∃ x, f x = g x
-- Mathlib.Algebra.Group.Hom.Defs
instOneOneHom.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : One M] [inst_1 : One N],
  instOneOneHom = { one := { toFun := fun x => 1, map_one' := ⋯ } }
-- Init.System.FilePath
/-- The string representation of the path.  -/
System.FilePath.toString : System.FilePath → String
-- Mathlib.Order.SupClosed
/-- Every set in a meet-semilattice generates a set closed under meet.  -/
infClosure : {α : Type u_3} → [SemilatticeInf α] → ClosureOperator (Set α)
-- Mathlib.Data.Set.Card
Set.fiber_ncard_ne_zero_iff_mem_image : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {y : β},
  autoParam s.Finite Set.fiber_ncard_ne_zero_iff_mem_image._auto_1 → ({x | x ∈ s ∧ f x = y}.ncard ≠ 0 ↔ y ∈ f '' s)
-- Mathlib.Algebra.Group.Basic
sub_one_nsmul_add : ∀ {M : Type u_4} [inst : AddMonoid M] {n : ℕ}, n ≠ 0 → ∀ (a : M), a + (n - 1) • a = n • a
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
Set.Subsingleton.threeGPFree : ∀ {α : Type u_2} [inst : Monoid α] {s : Set α}, s.Subsingleton → ThreeGPFree s
-- Mathlib.Data.Real.Embedding
Archimedean.ratLt.eq_1 : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : One M] (x : M),
  Archimedean.ratLt x = {r | r.num • 1 < r.den • x}
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.toList.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp]
  (t t_1 : Std.ExtDTreeMap α (fun x => β) cmp),
  t = t_1 → Std.ExtDTreeMap.Const.toList t = Std.ExtDTreeMap.Const.toList t_1
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.coe_eq_univ : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L : BooleanSubalgebra α}, ↑L = Set.univ ↔ L = ⊤
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.replaceFTR.go.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Array α → Sort u_2) (x : α) (xs : List α) (acc : Array α)
  (h_1 : (acc : Array α) → motive [] acc) (h_2 : (x : α) → (xs : List α) → (acc : Array α) → motive (x :: xs) acc),
  (match x :: xs, acc with
    | [], acc => h_1 acc
    | x :: xs, acc => h_2 x xs acc) =
    h_2 x xs acc
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.nontrivial_iff : ∀ {M : Type u_1} [inst : AddZeroClass M], Nontrivial (AddSubmonoid M) ↔ Nontrivial M
-- Mathlib.MeasureTheory.Measure.Count
MeasureTheory.Measure.count_real_univ : ∀ {α : Type u_1} [inst : MeasurableSpace α], MeasureTheory.Measure.count.real Set.univ = ↑(Nat.card α)
-- Batteries.Data.Array.Scan
Array.getElem?_scanr_zero : ∀ {α : Type u_1} {β : Type u_2} {init : β} {as : Array α} {f : α → β → β},
  (Array.scanr f init as)[0]? = some (Array.foldr f init as)
-- Mathlib.Order.Filter.Pointwise
Filter.Tendsto.inv_inv : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : DivisionMonoid β] [inst_2 : FunLike F α β]
  [MonoidHomClass F α β] (m : F) {f₁ : Filter α} {f₂ : Filter β},
  Filter.Tendsto (⇑m) f₁ f₂ → Filter.Tendsto (⇑m) f₁⁻¹ f₂⁻¹
-- Batteries.Data.BinomialHeap.Basic
/-- The conditions under which `findMin` is well-formed.  -/
Batteries.BinomialHeap.Imp.Heap.WF.findMin : {α : Type u_1} →
  {le : α → α → Bool} →
    {n : ℕ} →
      {k : Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.Heap α} →
        {res : Batteries.BinomialHeap.Imp.FindMin α} →
          {s : Batteries.BinomialHeap.Imp.Heap α} →
            Batteries.BinomialHeap.Imp.Heap.WF le n s →
              Batteries.BinomialHeap.Imp.FindMin.WF le res →
                (∀ {s : Batteries.BinomialHeap.Imp.Heap α},
                    Batteries.BinomialHeap.Imp.Heap.WF le n s → Batteries.BinomialHeap.Imp.Heap.WF le 0 (k s)) →
                  Batteries.BinomialHeap.Imp.FindMin.WF le (Batteries.BinomialHeap.Imp.Heap.findMin le k s res)
-- Mathlib.RingTheory.FiniteType
/-- A commutative algebra is finitely generated if and only if it is a quotient of a polynomial ring
in `n` variables.  -/
Algebra.FiniteType.iff_quotient_mvPolynomial'' : ∀ {R : Type uR} {S : Type uS} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
  Algebra.FiniteType R S ↔ ∃ n f, Function.Surjective ⇑f
-- Mathlib.RingTheory.Localization.Basic
Localization.algEquiv_mk' : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (x : R) (y : ↥M),
  (Localization.algEquiv M S) (IsLocalization.mk' (Localization M) x y) = IsLocalization.mk' S x y
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.isRkFinite_ground : ∀ {α : Type u_1} (M : Matroid α) [M.RankFinite], M.IsRkFinite M.E
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.le_order_iff_forall : ∀ {Γ : Type u_1} {R : Type u_3} [inst : Zero R] [inst_1 : LinearOrder Γ] [inst_2 : Zero Γ] {x : HahnSeries Γ R} {i : Γ},
  x ≠ 0 → (i ≤ x.order ↔ ∀ j < i, x.coeff j = 0)
-- Mathlib.Algebra.Group.Defs
/-- An additive monoid in which addition is right-cancellative.
Main examples are `ℕ` and groups. This is the right typeclass for many sum lemmas, as having a zero
is useful to define the sum over the empty set, so `AddRightCancelSemigroup` is not enough.  -/
AddRightCancelMonoid : Type u → Type u
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.instEpiGCcSc : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' : κ) (i₀ i₁ i₂ i₃ i₃' : ι) (hi₀ : i₀ = data.i₀ r pq' ⋯)
  (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯) (hi₃' : i₃' = data.i₃ r' pq' ⋯)
  (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq') (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂),
  CategoryTheory.Epi
    (CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.ccSc X data r r' hrr' hr pq pq' i₀ i₁ i₂ i₃ i₃'
        hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' hn₁ hn₂).g
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.π_truncGTIsoTruncGE_inv_assoc : ∀ {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 : ℤ) (h : a + 1 = b) {Z : CategoryTheory.Functor C C}
  (h_1 : t.truncGT a ⟶ Z),
  CategoryTheory.CategoryStruct.comp (t.truncGEπ b)
      (CategoryTheory.CategoryStruct.comp (t.truncGTIsoTruncGE a b h).inv h_1) =
    CategoryTheory.CategoryStruct.comp (t.truncGTπ a) h_1
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.support_ofFintype : ∀ {α : Type u_1} [inst : Fintype α] {f : α → ENNReal} (h : ∑ a, f a = 1),
  (PMF.ofFintype f h).support = Function.support f
-- Init.Grind.Ring.Basic
Lean.Grind.Ring.intCast_mul_left_comm : ∀ {α : Type u} [inst : Lean.Grind.Ring α] (a : α) (b : ℤ) (c : α), a * (↑b * c) = ↑b * (a * c)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- `⊥`, coerced to a set, is the empty set.  -/
AffineSubspace.bot_coe : ∀ (k : Type u_1) (V : Type u_2) (P : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P], ↑⊥ = ∅
-- Batteries.Tactic.Lint.Simp
/-- The result of replacement  -/
Batteries.Tactic.Lint.SimpTheoremInfo.rhs : Batteries.Tactic.Lint.SimpTheoremInfo → Lean.Expr
-- Mathlib.Algebra.Ring.IsFormallyReal
IsSumNonzeroSq.add : ∀ {R : Type u_1} [inst : AddMonoid R] [inst_1 : Mul R] {s₁ s₂ : R},
  IsSumNonzeroSq s₁ → IsSumNonzeroSq s₂ → IsSumNonzeroSq (s₁ + s₂)
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebra_obj_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat))
  {ι : Type t} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) (M : ↑(F.obj { as := Opposite.op S }).obj) (i₁ i₂ : ι),
  ((F.toDescentDataAsCoalgebra f).obj M).hom i₁ i₂ =
    (F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).adj.unit.toNatTrans.app M)
-- Mathlib.Combinatorics.Additive.CauchyDavenport
/-- A generalisation of the **Cauchy-Davenport theorem** to arbitrary groups. The size of `s * t` is
lower-bounded by `|s| + |t| - 1` unless this quantity is greater than the size of the smallest
subgroup.  -/
cauchy_davenport_minOrder_mul : ∀ {α : Type u_2} [inst : Group α] [inst_1 : DecidableEq α] {s t : Finset α},
  s.Nonempty → t.Nonempty → min (Monoid.minOrder α) ↑(s.card + t.card - 1) ≤ ↑(s * t).card
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
Submodule.restrictScalars_restrictScalars : ∀ (S : Type u_1) {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Semiring S]
  [inst_3 : Module S M] [inst_4 : Module R M] [inst_5 : SMul S R] [inst_6 : IsScalarTower S R M] (T : Type u_4)
  [inst_7 : Semiring T] [inst_8 : SMul T R] [inst_9 : SMul S T] [inst_10 : Module T M] [inst_11 : IsScalarTower S T M]
  [inst_12 : IsScalarTower T R M] (V : Submodule R M),
  Submodule.restrictScalars S (Submodule.restrictScalars T V) = Submodule.restrictScalars S V
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
CategoryTheory.Limits.hasPushout_of_left_factors_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y : C} (h : W ⟶ X) [CategoryTheory.Epi h] (f : X ⟶ Y),
  CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp h f) h
-- Mathlib.Data.Fintype.List
Multiset.mem_lists_iff : ∀ {α : Type u_1} (s : Multiset α) (l : List α), l ∈ s.lists ↔ s = ⟦l⟧
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.instFullMonCatForget₂AddMonoidHomCarrierCarrier : (CategoryTheory.forget₂ AddCommMonCat AddMonCat).Full