mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_X_pow_mul' : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n d : ℕ),
  (Polynomial.X ^ n * p).coeff d = if n ≤ d then p.coeff (d - n) else 0
-- Init.Data.Nat.Power2.Basic
_private.Init.Data.Nat.Power2.Basic.0.Nat.nextPowerOfTwo.go.congr_simp : ∀ (n n_1 : ℕ),
  n = n_1 →
    ∀ (power power_1 : ℕ) (e_power : power = power_1) (h : power > 0),
      Nat.nextPowerOfTwo.go✝ n power h = Nat.nextPowerOfTwo.go✝ n_1 power_1 ⋯
-- Mathlib.Order.SuccPred.Limit
IsLUB.isSuccPrelimit_of_notMem : ∀ {α : Type u_1} {a : α} [inst : LinearOrder α] {s : Set α}, IsLUB s a → a ∉ s → Order.IsSuccPrelimit a
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k a fallback : α} {v : β k},
  Std.Internal.List.getKeyD a (Std.Internal.List.insertEntry k v l) fallback =
    if (k == a) = true then k else Std.Internal.List.getKeyD a l fallback
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- **Alias** of the reverse direction of `SimpleGraph.isContained_congr_left`. -/
SimpleGraph.IsContained.congr_left : ∀ {α : Type u_4} {β : Type u_5} {γ : Type u_6} {A : SimpleGraph α} {B : SimpleGraph β} {C : SimpleGraph γ}
  (e₁ : A ≃g B), B.IsContained C → A.IsContained C
-- Mathlib.Combinatorics.Enumerative.Pentagonal.Ring
/-- By summing with telescoping, we get a recurrence formula for $A$

$$ A_k = 1 - x^{2k + 3} - x^{3k + 5}A_{k + 1} $$
 -/
_private.Mathlib.Combinatorics.Enumerative.Pentagonal.Ring.0.Pentagonal.tsum_powMulProdOneSubPow : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : TopologicalSpace R] [IsTopologicalRing R] [T2Space R] (k : ℕ) {x : R},
  IsTopologicallyNilpotent x →
    (∀ (k : ℕ), Summable fun x_1 => Pentagonal.powMulProdOneSubPow✝ k x_1 x) →
      (∀ (k : ℕ), Multipliable fun n => 1 - x ^ (n + k + 1)) →
        ∑' (n : ℕ), Pentagonal.powMulProdOneSubPow✝ k n x =
          1 - x ^ (2 * k + 3) - x ^ (3 * k + 5) * ∑' (n : ℕ), Pentagonal.powMulProdOneSubPow✝ (k + 1) n x
-- Mathlib.Algebra.Lie.Solvable
_private.Mathlib.Algebra.Lie.Solvable.0.LieAlgebra.derivedAbelianOfIdeal.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (k : ℕ) → motive k.succ),
  (match 0 with
    | 0 => h_1 ()
    | k.succ => h_2 k) =
    h_1 ()
-- Mathlib.Analysis.BoundedVariation
/-- Eta-expanded form of `BoundedVariationOn.mul` -/
BoundedVariationOn.fun_mul : ∀ {α : Type u_2} [inst : LinearOrder α] {f g : α → ℝ} {s : Set α},
  BoundedVariationOn f s → BoundedVariationOn g s → BoundedVariationOn (fun i => f i * g i) s
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.mk : {M : Type u_1} →
  [inst : Add M] →
    (toSetoid : Setoid M) → (∀ {w x y z : M}, toSetoid w x → toSetoid y z → toSetoid (w + y) (x + z)) → AddCon M
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.zero_ne_one_of_char0 : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] [Lean.Grind.IsCharP α 0] (ctx : Lean.Grind.Linarith.Context α)
  (p : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.zero_ne_one_cert p = true →
    Lean.Grind.Linarith.Var.denote ctx 0 = One.one → Lean.Grind.Linarith.Poly.denote' ctx p ≠ 0
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
/-- the natural transformations between the base components  -/
CategoryTheory.Limits.CatCospanTransformMorphism.base : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      {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} →
                      [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'} →
                                {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} →
                                  CategoryTheory.Limits.CatCospanTransformMorphism ψ ψ' → (ψ.base ⟶ ψ'.base)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsNeg.not_AllZero : ∀ {li : Tactic.ComputeAsymptotics.UnitMonomial}, li.FirstNonzeroIsNeg → ¬li.AllZero
-- Mathlib.Algebra.Group.Pi.Basic
Pi.instIsCancelMul : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → Mul (f i)] [∀ (i : I), IsCancelMul (f i)],
  IsCancelMul ((i : I) → f i)
-- Mathlib.Algebra.Homology.DerivedCategory.TStructure
DerivedCategory.exists_iso_Q_obj_of_isGE_of_isLE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (X : DerivedCategory C) (a b : ℤ) [X.IsGE a] [X.IsLE b],
  ∃ K, ∃ (_ : K.IsStrictlyGE a) (_ : K.IsStrictlyLE b), Nonempty (X ≅ DerivedCategory.Q.obj K)
-- Mathlib.Data.Finset.Sort
Finset.orderEmbOfFin.congr_simp : ∀ {α : Type u_1} [inst : LinearOrder α] (s s_1 : Finset α) (e_s : s = s_1) {k : ℕ} (h : s.card = k),
  s.orderEmbOfFin h = s_1.orderEmbOfFin ⋯
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.image_connectedComponentIn : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} (h : X ≃ₜ Y)
  {x : X}, x ∈ s → ⇑h '' connectedComponentIn s x = connectedComponentIn (⇑h '' s) (h x)
-- Mathlib.Probability.Distributions.Beta
ProbabilityTheory.beta.eq_1 : ∀ (α β : ℝ), ProbabilityTheory.beta α β = Real.Gamma α * Real.Gamma β / Real.Gamma (α + β)
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.withConstants_self_expansion : ∀ (L : FirstOrder.Language) {M : Type w} [inst : L.Structure M], (L.lhomWithConstants M).IsExpansionOn M
-- Mathlib.Tactic.NormNum.Ordinal
Mathlib.Meta.NormNum.isNat_ordinalMul : ∀ {a b : Ordinal.{u}} {an bn rn : ℕ},
  Mathlib.Meta.NormNum.IsNat a an →
    Mathlib.Meta.NormNum.IsNat b bn → an * bn = rn → Mathlib.Meta.NormNum.IsNat (a * b) rn
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_union_add_inter : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α),
  MeasurableSet t → μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.mem_sSup_of_mem : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {S : Set (Submodule R M)} {s : Submodule R M}, s ∈ S → ∀ {x : M}, x ∈ s → x ∈ sSup S
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.mk.congr_simp : ∀ {α : Type u_3} [inst : MeasurableSpace α] {M : Type u_4} [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  (measureOf' measureOf'_1 : Set α → M) (e_measureOf' : measureOf' = measureOf'_1) (empty' : measureOf' ∅ = 0)
  (not_measurable' : ∀ ⦃i : Set α⦄, ¬MeasurableSet i → measureOf' i = 0)
  (m_iUnion' :
    ∀ ⦃f : ℕ → Set α⦄,
      (∀ (i : ℕ), MeasurableSet (f i)) →
        Pairwise (Function.onFun Disjoint f) → HasSum (fun i => measureOf' (f i)) (measureOf' (⋃ i, f i))),
  { measureOf' := measureOf', empty' := empty', not_measurable' := not_measurable', m_iUnion' := m_iUnion' } =
    { measureOf' := measureOf'_1, empty' := ⋯, not_measurable' := ⋯, m_iUnion' := ⋯ }
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey_insertIfNew : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h : (↑m).WF) {k a : α} {v : β k}
  {h₁ : (m.insertIfNew k v).contains a = true},
  (m.insertIfNew k v).getKey a h₁ = if h₂ : (k == a) = true ∧ m.contains k = false then k else m.getKey a ⋯
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.atBot_of_mul_const_le : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelMonoid M] {l : Filter α}
  {f g : α → M},
  (∃ C, ∀ (x : α), C ≤ g x) → Filter.Tendsto (fun x => f x * g x) l Filter.atBot → Filter.Tendsto f l Filter.atBot
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.instInsertSigmaOfBEqOfHashable : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable α] → Insert ((a : α) × β a) (Std.DHashMap.Raw α β)
-- Mathlib.RepresentationTheory.Subrepresentation
Subrepresentation.submoduleSubrepresentationOrderIso_symm_apply : ∀ {A : Type u_1} {G : Type u_2} {M : Type u_4} [inst : CommSemiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid M]
  [inst_3 : Module (MonoidAlgebra A G) M] (σ : Subrepresentation (Representation.ofModule M)),
  (RelIso.symm Subrepresentation.submoduleSubrepresentationOrderIso) σ = σ.asSubmodule'
-- Mathlib.Algebra.Order.Floor.Extended
ENat.floor_natCast : ∀ (n : ℕ∞), ⌊↑n⌋ₑ = n
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- A snake input in an abelian category `C` consists of morphisms
of short complexes `L₀ ⟶ L₁ ⟶ L₂ ⟶ L₃` (which should be visualized vertically) such
that `L₀` and `L₃` are respectively the kernel and the cokernel of `L₁ ⟶ L₂`,
`L₁` and `L₂` are exact, `L₁.g` is epi and `L₂.f` is mono.  -/
CategoryTheory.ShortComplex.SnakeInput : (C : Type u_1) → [inst : CategoryTheory.Category.{v_1, u_1} C] → [CategoryTheory.Abelian C] → Type (max u_1 v_1)
-- Std.Data.ExtTreeMap.Basic
/-- Modifies in place the value associated with a given key.

This function ensures that the value is used linearly.
 -/
Std.ExtTreeMap.modify : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → α → (β → β) → Std.ExtTreeMap α β cmp
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.Adjunction.homEquiv₂_apply : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {l : b ⟶ c} {r : c ⟶ b}
  (adj : CategoryTheory.Bicategory.Adjunction l r) {g : a ⟶ b} {h : a ⟶ c}
  (α : CategoryTheory.CategoryStruct.comp g l ⟶ h),
  adj.homEquiv₂ α =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor g).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft g adj.unit)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator g l r).inv
          (CategoryTheory.Bicategory.whiskerRight α r)))
-- Init.Data.Nat.Lemmas
Nat.mul_mod_mul_right : ∀ (z x y : ℕ), x * z % (y * z) = x % y * z
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.coe_intCast : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : IntCast β] (n : ℤ), ⇑↑n = fun x => ↑n
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.RightExtension.mk_left : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : L.comp F' ⟶ F), (CategoryTheory.Functor.RightExtension.mk F' α).left = F'
-- Init.Data.Vector.Lemmas
Vector.append_left_inj : ∀ {α : Type u_1} {n m : ℕ} {xs₁ xs₂ : Vector α n} (ys : Vector α m), xs₁ ++ ys = xs₂ ++ ys ↔ xs₁ = xs₂
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.revAt.eq_1 : ∀ (N : ℕ), Polynomial.revAt N = { toFun := fun i => if i ≤ N then N - i else i, inj' := ⋯ }
-- Mathlib.Data.ENNReal.Basic
/-- `(1 : ℝ≥0∞) ≤ 2`, recorded as a `Fact` for use with `Lp` spaces.  -/
fact_one_le_two_ennreal : Fact (1 ≤ 2)
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.productMap_left_apply : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : CommSemiring S] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R S]
  (f : A →ₐ[R] S) (g : B →ₐ[R] S) (a : A), (Algebra.TensorProduct.productMap f g) (a ⊗ₜ[R] 1) = f a
-- Mathlib.AlgebraicGeometry.OrderOfVanishing
AlgebraicGeometry.Scheme.ordHom.eq_1 : ∀ {X : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsIntegral X]
  [inst_1 : AlgebraicGeometry.IsLocallyNoetherian X] (z : ↥X) (hz : Order.coheight z = 1),
  AlgebraicGeometry.Scheme.ordHom z hz = Ring.ordFrac ↑(X.presheaf.stalk z)
-- Std.Tactic.BVDecide.LRAT.Internal.CNF
Std.Tactic.BVDecide.LRAT.Internal.Clause.sat_iff_exists : ∀ {α : Type u_1} {β : Type u_2} [inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β] (p : α → Bool) (c : β),
  Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p c ↔
    ∃ l ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c, Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p l
-- Mathlib.Algebra.Colimit.Module
AddCommGroup.DirectLimit.lift.congr_simp : ∀ {ι : Type u_2} [inst : Preorder ι] (G : ι → Type u_3) [inst_1 : (i : ι) → AddCommMonoid (G i)]
  (f : (i j : ι) → i ≤ j → G i →+ G j) [inst_2 : DecidableEq ι] (P : Type u_4) [inst_3 : AddCommMonoid P]
  (g g_1 : (i : ι) → G i →+ P) (e_g : g = g_1)
  (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x),
  AddCommGroup.DirectLimit.lift G f P g Hg = AddCommGroup.DirectLimit.lift G f P g_1 ⋯
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.ofHom_apply : ∀ {X Y : Type u} [inst : AddMonoid X] [inst_1 : AddMonoid Y] (f : X →+ Y) (x : X),
  (CategoryTheory.ConcreteCategory.hom (AddMonCat.ofHom f)) x = f x
-- Init.GrindInstances.ToInt
Lean.Grind.instToIntBitVecUint : {v : ℕ} → Lean.Grind.ToInt (BitVec v) (Lean.Grind.IntInterval.uint v)
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.XXIsoOfEq_inv_ιTotal_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  {x₁ y₁ : I₁} (h₁ : x₁ = y₁) {x₂ y₂ : I₂} (h₂ : x₂ = y₂) (i₁₂ : I₁₂) (h : c₁.π c₂ c₁₂ (x₁, x₂) = i₁₂) {Z : C}
  (h_1 : (K.total c₁₂).X i₁₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.XXIsoOfEq C c₁ c₂ K h₁ h₂).inv
      (CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ x₁ x₂ i₁₂ h) h_1) =
    CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ y₁ y₂ i₁₂ ⋯) h_1
-- Mathlib.Data.List.Destutter
List.destutter_nil : ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R], List.destutter R [] = []
-- Std.Data.Internal.List.Associative
Std.Internal.List.forM_eq_forM_toProd : ∀ {α : Type u} {β : Type v} {m' : Type w → Type w'} [inst : Monad m'] [LawfulMonad m'] {l : List ((_ : α) × β)}
  {f : α → β → m' PUnit.{w + 1}},
  (forM l fun a => f a.fst a.snd) = forM (List.map (fun x => (x.fst, x.snd)) l) fun a => f a.1 a.2
-- Mathlib.Data.Semiquot
/-- If `f` is a constant on `q.s`, then `q.liftOn f` is the value of `f`
at any point of `q`.  -/
Semiquot.liftOn : {α : Type u_1} → {β : Type u_2} → (q : Semiquot α) → (f : α → β) → (∀ a ∈ q, ∀ b ∈ q, f a = f b) → β
-- Lean.Parser.Do
Lean.Parser.Term.doUnless : Lean.Parser.Parser
-- Aesop.Util.Tactic
/-- Introduce as many binders as possible while unfolding definitions with the
ambient transparency.  -/
Aesop.introsUnfolding : Lean.MVarId → Lean.MetaM (Array Lean.FVarId × Lean.MVarId)
-- Mathlib.NumberTheory.LSeries.Basic
/-- `LSeriesSummable f s` indicates that the L-series of `f` converges absolutely at `s`.  -/
LSeriesSummable : (ℕ → ℂ) → ℂ → Prop
-- Mathlib.Data.Set.Function
Subtype.coind_bijective : ∀ {α : Type u_7} {β : Type u_8} {f : α → β} {p : Set β} (h : ∀ (a : α), f a ∈ p),
  Function.Injective f → Set.SurjOn f Set.univ p → Function.Bijective (Subtype.coind f h)
-- Lean.Parser.Module
Lean.Parser.ModuleParserState.pos : Lean.Parser.ModuleParserState → String.Pos.Raw
-- Mathlib.Order.Monotone.Extension
/-- If a function is antitone and is bounded on a set `s`, then it admits an antitone extension to
the whole space.  -/
AntitoneOn.exists_antitone_extension : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β] {f : α → β}
  {s : Set α}, AntitoneOn f s → BddBelow (f '' s) → BddAbove (f '' s) → ∃ g, Antitone g ∧ Set.EqOn f g s
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `TendstoUniformlyOnFilter.neg` -/
TendstoUniformlyOnFilter.fun_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3}
  {l : Filter ι} {l' : Filter β} {f : ι → β → α} {g : β → α},
  TendstoUniformlyOnFilter f g l l' → TendstoUniformlyOnFilter (fun i i_1 => -f i i_1) (fun i => -g i) l l'
-- Init.Data.List.Basic
List.zipWith_nil_right : ∀ {α : Type u} {β : Type v} {γ : Type w} {l : List α} {f : α → β → γ}, List.zipWith f l [] = []
-- Mathlib.Order.MinMax
min_le_min : ∀ {α : Type u} [inst : LinearOrder α] {a b c d : α}, c ≤ a → d ≤ b → min c d ≤ min a b
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.UnitaryGroup.toGL_one : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v} [inst_2 : CommRing α] [inst_3 : StarRing α],
  Matrix.UnitaryGroup.toGL 1 = 1
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- Translate a finite pattern `p` so that it occurs at the translate `v`, before completing into
a configuration.

On input `h : G`, we proceed as follows:
* if `h` lies in the left-translate of the support, i.e. `h ∈ p.support.image (v * ·)`,
  choose (noncomputably) `w ∈ p.support` with `v * w = h` and return `p.config w`;
* otherwise return `default`.

This definition does not assume left-cancellation; it only *chooses* a preimage.
Uniqueness (and the usual equations such as `Pattern.mulShift p v (v * w) = p.config w`)
require a left-cancellation hypothesis and are proved in separate lemmas.
 -/
SymbolicDynamics.FullShift.Pattern.mulShift : {A : Type u_1} → [inst : Inhabited A] → {G : Type u_2} → [Monoid G] → SymbolicDynamics.FullShift.Pattern A G → G → G → A
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- A bounded convergence theorem for a finite measure:
If a sequence of bounded continuous non-negative functions are uniformly bounded by a constant and
tend pointwise to a limit, then their integrals (`MeasureTheory.FiniteMeasure.testAgainstNN`)
against the finite measure tend to the integral of the limit.

Related results:
* `MeasureTheory.FiniteMeasure.tendsto_testAgainstNN_filter_of_le_const`:
  more general assumptions
* `MeasureTheory.FiniteMeasure.tendsto_lintegral_nn_of_le_const`:
  using `MeasureTheory.lintegral` for integration.
 -/
MeasureTheory.FiniteMeasure.tendsto_testAgainstNN_of_le_const : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [OpensMeasurableSpace Ω]
  {μ : MeasureTheory.FiniteMeasure Ω} {fs : ℕ → BoundedContinuousFunction Ω NNReal} {c : NNReal},
  (∀ (n : ℕ) (ω : Ω), (fs n) ω ≤ c) →
    ∀ {f : BoundedContinuousFunction Ω NNReal},
      (∀ (ω : Ω), Filter.Tendsto (fun n => (fs n) ω) Filter.atTop (nhds (f ω))) →
        Filter.Tendsto (fun n => μ.testAgainstNN (fs n)) Filter.atTop (nhds (μ.testAgainstNN f))
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.toBasis.eq_1 : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] (b : OrthonormalBasis ι 𝕜 E),
  b.toBasis = Module.Basis.ofEquivFun (b.repr.trans (WithLp.linearEquiv 2 𝕜 (ι → 𝕜)))
-- Mathlib.Data.W.Constructions
_private.Mathlib.Data.W.Constructions.0.WType.toList.match_1.splitter : (γ : Type u_1) →
  (motive : WType (WType.Listβ γ) → Sort u_2) →
    (x : WType (WType.Listβ γ)) →
      ((f : WType.Listβ γ WType.Listα.nil → WType (WType.Listβ γ)) → motive (WType.mk WType.Listα.nil f)) →
        ((hd : γ) →
            (f : WType.Listβ γ (WType.Listα.cons hd) → WType (WType.Listβ γ)) →
              motive (WType.mk (WType.Listα.cons hd) f)) →
          motive x
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.Y_eq_of_Y_ne' : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  W'.Equation P →
    W'.Equation Q → P 2 ≠ 0 → Q 2 ≠ 0 → P 0 * Q 2 = Q 0 * P 2 → P 1 * Q 2 ≠ W'.negY Q * P 2 → P 1 * Q 2 = Q 1 * P 2
-- Mathlib.Geometry.Manifold.HasGroupoid
/-- An open embedding of `α` into `H` induces an `H`-charted space structure on `α`.
See `OpenPartialHomeomorph.singletonChartedSpace`.  -/
Topology.IsOpenEmbedding.singletonChartedSpace : {H : Type u} →
  [inst : TopologicalSpace H] →
    {α : Type u_5} →
      [inst_1 : TopologicalSpace α] → [Nonempty α] → {f : α → H} → Topology.IsOpenEmbedding f → ChartedSpace H α
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.instMin.eq_1 : ∀ {G : Type u_1} [inst : Group G],
  Subgroup.instMin =
    {
      min := fun H₁ H₂ =>
        let __src := H₁.toSubmonoid ⊓ H₂.toSubmonoid;
        { toSubmonoid := __src, inv_mem' := ⋯ } }
-- Lean.Elab.Do.Control
/-- Build a `DoElemCont` that unpacks the lifted body's result and resumes `origCont.k`.  -/
Lean.Elab.Do.EffectForwarder.restoreCont : Lean.Elab.Do.EffectForwarder → Lean.Elab.Do.DoElabM Lean.Elab.Do.DoElemCont
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SyntheticMVarDecl.mk.inj : ∀ {stx : Lean.Syntax} {kind : Lean.Elab.Term.SyntheticMVarKind} {stx_1 : Lean.Syntax}
  {kind_1 : Lean.Elab.Term.SyntheticMVarKind},
  { stx := stx, kind := kind } = { stx := stx_1, kind := kind_1 } → stx = stx_1 ∧ kind = kind_1
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_withDensity_iff_integrable_smul₀ : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_8} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : α → NNReal},
  AEMeasurable f μ →
    ∀ {g : α → E},
      MeasureTheory.Integrable g (μ.withDensity fun x => ↑(f x)) ↔ MeasureTheory.Integrable (fun x => f x • g x) μ
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- A set of points is cospherical in an affine subspace `S₁` if and only if its image under the
inclusion into a larger affine subspace `S₂` is cospherical.  -/
EuclideanGeometry.Cospherical.inclusion_iff : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {S₁ S₂ : AffineSubspace ℝ P} [inst_4 : Nonempty ↥S₁] {ps : Set ↥S₁}
  [S₁.direction.HasOrthogonalProjection] [S₂.direction.HasOrthogonalProjection] (hS : S₁ ≤ S₂),
  EuclideanGeometry.Cospherical (⇑(AffineSubspace.inclusion hS) '' ps) ↔ EuclideanGeometry.Cospherical ps
-- Mathlib.Topology.UniformSpace.Defs
symmetrize_mem_uniformity : ∀ {α : Type ua} [inst : UniformSpace α] {V : SetRel α α}, V ∈ uniformity α → V.symmetrize ∈ uniformity α
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
div_lt_div_right' : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulRightStrictMono α] {a b : α}, a < b → ∀ (c : α), a / c < b / c
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.mem_dpEqualizer_iff : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} (hI hI' : DividedPowers I) {x : A},
  x ∈ hI.dpEqualizer hI' ↔ x ∈ I ∧ ∀ (n : ℕ), hI.dpow n x = hI'.dpow n x
-- Mathlib.Geometry.Euclidean.Projection
/-- A point is its own reflection if and only if it is in the subspace.  -/
EuclideanGeometry.reflection_eq_self_iff : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {s : AffineSubspace 𝕜 P}
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] (p : P),
  (EuclideanGeometry.reflection s) p = p ↔ p ∈ s
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.fap.inj : ∀ {c : Lean.IR.FunId} {ys : Array Lean.IR.Arg} {c_1 : Lean.IR.FunId} {ys_1 : Array Lean.IR.Arg},
  Lean.IR.Expr.fap c ys = Lean.IR.Expr.fap c_1 ys_1 → c = c_1 ∧ ys = ys_1
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.symm_commAlgEquiv : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Monoid M] [inst_4 : Monoid N],
  (MonoidAlgebra.commAlgEquiv R).symm = MonoidAlgebra.commAlgEquiv R