mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Nat.Choose.Multinomial
Nat.multinomial_congr : ∀ {α : Type u_1} {s : Finset α} {f g : α → ℕ}, (∀ a ∈ s, f a = g a) → Nat.multinomial s f = Nat.multinomial s g
-- Mathlib.Geometry.Euclidean.Altitude
Affine.Simplex.height_restrict : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (S : AffineSubspace ℝ P)
  (hS : affineSpan ℝ (Set.range s.points) ≤ S) (i : Fin (n + 1)), (s.restrict S hS).height i = s.height i
-- Mathlib.GroupTheory.Exponent
Monoid.one_lt_exponent : ∀ {G : Type u} [inst : LeftCancelMonoid G] [Finite G] [Nontrivial G], 1 < Monoid.exponent G
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.logMahlerMeasure_one : Polynomial.logMahlerMeasure 1 = 0
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.compl.eq_1 : ∀ {α : Type u_1} [inst : LE α] (s : LowerSet α), s.compl = { carrier := (↑s)ᶜ, upper' := ⋯ }
-- Aesop.Rule
Aesop.Safety.noConfusionType : Sort v✝ → Aesop.Safety → Aesop.Safety → Sort v✝
-- Mathlib.Algebra.Group.Units.Basic
AddUnits.eq_neg_of_add_eq_zero_left : ∀ {α : Type u} [inst : AddMonoid α] {u : AddUnits α} {a : α}, ↑u + a = 0 → a = ↑(-u)
-- Plausible.Arbitrary
Plausible.Bool.Arbitrary : Plausible.Arbitrary Bool
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_eq_self : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] {s : Set α} {f : α → M}, s.indicator f = f ↔ Function.support f ⊆ s
-- Mathlib.NumberTheory.BernoulliPolynomials
Polynomial.derivative_bernoulli_add_one : ∀ (k : ℕ), Polynomial.derivative (Polynomial.bernoulli (k + 1)) = (↑k + 1) * Polynomial.bernoulli k
-- Batteries.Data.Nat.Lemmas
Nat.recDiagOn_zero_zero : ∀ {motive : ℕ → ℕ → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : ℕ) → motive 0 n → motive 0 (n + 1))
  (succ_zero : (m : ℕ) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : ℕ) → motive m n → motive (m + 1) (n + 1)),
  Nat.recDiagOn 0 0 zero_zero zero_succ succ_zero succ_succ = zero_zero
-- Mathlib.MeasureTheory.SetAlgebra
/-- An algebra of sets is a family of sets containing the empty set and closed by complement and
union. Consequently it is also closed by difference (see `IsSetAlgebra.sdiff_mem`) and intersection
(see `IsSetAlgebra.inter_mem`).  -/
MeasureTheory.IsSetAlgebra : {α : Type u_1} → Set (Set α) → Prop
-- Mathlib.FieldTheory.Perfect
frobenius_comp_frobeniusEquiv_symm : ∀ (R : Type u_1) (p : ℕ) [inst : CommSemiring R] [inst_1 : ExpChar R p] [inst_2 : PerfectRing R p],
  (frobenius R p).comp ↑(frobeniusEquiv R p).symm = RingHom.id R
-- Mathlib.LinearAlgebra.InvariantBasisNumber
/-- Nontrivial commutative rings satisfy the invariant basis number property.

There are two stronger results in mathlib:
1.  `CommRing.orzechProperty` in `Mathlib.RingTheory.FiniteType`,
    which says that any commutative ring satisfies the Orzech property, and hence
    (by `strongRankCondition_of_orzechProperty`) that nontrivial commutative rings satisfy
    the strong rank condition. A shortcut instance `commRing_strongRankCondition` is also provided.
2.  `rankCondition_of_nontrivial_of_commSemiring` in
    `Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber`, which says that
    any nontrivial commutative semiring satisfies the rank condition.

We prove this instance here anyway to reduce the required imports.
 -/
invariantBasisNumber_of_nontrivial_of_commRing : ∀ {R : Type u} [inst : CommRing R] [Nontrivial R], InvariantBasisNumber R
-- Mathlib.Data.Fintype.Card
Fintype.card.eq_1 : ∀ (α : Type u_4) [inst : Fintype α], Fintype.card α = Finset.univ.card
-- Mathlib.NumberTheory.Divisors
Nat.properDivisors_one : Nat.properDivisors 1 = ∅
-- Mathlib.Probability.Distributions.TwoValued
/-- If an `AEMeasurable` function is ae equal to `0` or `1`, then its integral is equal to the
measure of the set where it equals `1`.  -/
MeasureTheory.integral_of_ae_eq_zero_or_one : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  AEMeasurable X μ → (∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1) → ∫ (x : Ω), X x ∂μ = μ.real {ω | X ω = 1}
-- Mathlib.MeasureTheory.Measure.Stieltjes
/-- **Alias** of `Ioc_sdiff_botSet`. -/
Ioc_diff_botSet : ∀ {R : Type u_1} [inst : LinearOrder R] (a b : R), Set.Ioc a b \ botSet = Set.Ioc a b
-- Mathlib.Data.Fintype.Basic
pfunFintype : (p : Prop) → [Decidable p] → (α : p → Type u_4) → [(hp : p) → Fintype (α hp)] → Fintype ((hp : p) → α hp)
-- Mathlib.Tactic.Explode.Pretty
/-- Given all `Entries`, return the entire Fitch table.  -/
Mathlib.Explode.entriesToMessageData : Mathlib.Explode.Entries → Lean.MetaM Lean.MessageData
-- Init.Data.List.Find
List.lookup_replicate_self : ∀ {α : Type u_2} [inst : BEq α] {n : ℕ} {α_1 : Type u_1} {b : α_1} [ReflBEq α] {a : α},
  List.lookup a (List.replicate n (a, b)) = if n = 0 then none else some b
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.lift_comp : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {P : Type u_3}
  [inst_3 : CommSemiring P] (x : R) [inst_4 : IsLocalization.Away x S] {g : R →+* P} (hg : IsUnit (g x)),
  (IsLocalization.Away.lift x hg).comp (algebraMap R S) = g
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.expand_zero : ∀ {R : Type u} [inst : CommSemiring R] (f : Polynomial R),
  (Polynomial.expand R 0) f = Polynomial.C (Polynomial.eval 1 f)
-- Mathlib.Order.Cover
AntisymmRel.wcovBy : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, AntisymmRel (fun x1 x2 => x1 ≤ x2) a b → a ⩿ b
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.isConj_apply_apply : ∀ {K : Type u_1} [inst : Field K] {k : Type u_2} [inst_1 : Field k] [inst_2 : Algebra k K] {φ : K →+* ℂ} {σ : Gal(K/k)},
  NumberField.ComplexEmbedding.IsConj φ σ → ∀ (x : K), σ (σ x) = x
-- Lean.Elab.Do.Basic
/-- Build an `FVarAliasInfo` recording that the reassignment binding `id` aliases the original
`let mut` binding represented by `mutVar`.
 -/
Lean.Elab.Do.MutVar.mkAliasInfo : Lean.Elab.Do.MutVar → Lean.FVarId → Lean.Elab.FVarAliasInfo
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.num : ℤ → Int.Internal.Linear.Expr
-- Std.Time.Format.Modifier
/-- Exactly 12:00:00
 -/
Std.Time.ExtendedDayPeriod.noon : Std.Time.ExtendedDayPeriod
-- Init.Data.Format.Instances
instToFormatRaw : Std.ToFormat String.Pos.Raw
-- Mathlib.Order.Partition.Finpartition
/-- A `Finpartition` constructor which does not insist on `⊥` not being a part.  -/
Finpartition.ofErase : {α : Type u_1} →
  [inst : Lattice α] →
    [inst_1 : OrderBot α] →
      [DecidableEq α] → {a : α} → (parts : Finset α) → parts.SupIndep id → parts.sup id = a → Finpartition a
-- Mathlib.Algebra.Order.Group.End
RelIso.mul_apply : ∀ {α : Type u_1} {r : α → α → Prop} (e₁ e₂ : r ≃r r) (x : α), (e₁ * e₂) x = e₁ (e₂ x)
-- Mathlib.Data.Nat.BinaryRec
Nat.bit_true : Nat.bit true = fun x => 2 * x + 1
-- Std.Async.Signal
/-- Create a `Selector` that resolves once `s` has received the signal. Note that calling this function
does not start the signal waiter.
 -/
Std.Async.Signal.Waiter.selector : Std.Async.Signal.Waiter → Std.Async.Selector Unit
-- Init.Data.Dyadic.Basic
Dyadic.toRat.eq_3 : ∀ (n : ℤ) (k : ℕ) (hn : n % 2 = 1), (Dyadic.ofOdd n (Int.negSucc k) hn).toRat = ↑(n * ↑(2 ^ (k + 1)))
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
/-- An auxiliary result, superseded by `toLimit_surjective`  -/
ProfiniteGrp.denseRange_toLimit : ∀ (P : ProfiniteGrp.{u}), DenseRange ⇑(ProfiniteGrp.Hom.hom P.toLimit)
-- Mathlib.Topology.Order.MonotoneContinuity
/-- If a function `f` is strictly monotone on a right neighborhood of `a` and the image of this
neighborhood under `f` includes `Ioi (f a)`, then `f` is continuous at `a` from the right.  -/
StrictMonoOn.continuousWithinAt_right_of_surjOn : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] {f : α → β} {s : Set α} {a : α},
  StrictMonoOn f s → s ∈ nhdsWithin a (Set.Ici a) → Set.SurjOn f s (Set.Ioi (f a)) → ContinuousWithinAt f (Set.Ici a) a
-- Mathlib.Algebra.Group.Defs
add_assoc : ∀ {G : Type u_1} [inst : AddSemigroup G] (a b c : G), a + b + c = a + (b + c)
-- Mathlib.Data.Nat.Factorial.Basic
Nat.ascFactorialBinary.induct_unfolding : ∀ (motive : ℕ → ℕ → ℕ → Prop),
  (∀ (n : ℕ), motive n 0 1) →
    (∀ (n : ℕ), motive n 1 n) →
      (∀ (n n_1 : ℕ),
          motive n ((n_1 + 2) / 2) (n.ascFactorialBinary ((n_1 + 2) / 2)) →
            motive (n + (n_1 + 2) / 2) ((n_1 + 2 + 1) / 2)
                ((n + (n_1 + 2) / 2).ascFactorialBinary ((n_1 + 2 + 1) / 2)) →
              motive n n_1.succ.succ
                (n.ascFactorialBinary ((n_1 + 2) / 2) * (n + (n_1 + 2) / 2).ascFactorialBinary ((n_1 + 2 + 1) / 2))) →
        ∀ (n k : ℕ), motive n k (n.ascFactorialBinary k)
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.unitsSMulEquiv_apply : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : HNNExtension.NormalWord.TransversalPair G A B}
  (w : HNNExtension.NormalWord d),
  (HNNExtension.NormalWord.unitsSMulEquiv φ) w = HNNExtension.NormalWord.unitsSMul φ 1 w
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffSection.instAdd : {𝕜 : 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] →
                      {F : Type u_5} →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] →
                            {n : WithTop ℕ∞} →
                              {V : M → Type u_6} →
                                [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                  [inst_9 : (x : M) → TopologicalSpace (V x)] →
                                    [inst_10 : FiberBundle F V] →
                                      [inst_11 : (x : M) → AddCommGroup (V x)] →
                                        [inst_12 : (x : M) → Module 𝕜 (V x)] →
                                          [VectorBundle 𝕜 F V] → Add (ContMDiffSection I F n V)
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.preimage_spanningSetsIndex_singleton : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite μ] (n : ℕ),
  MeasureTheory.spanningSetsIndex μ ⁻¹' {n} = disjointed (MeasureTheory.spanningSets μ) n
-- Mathlib.Data.Set.NAry
Set.image2_insert_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {a : α},
  Set.image2 f (insert a s) t = (fun b => f a b) '' t ∪ Set.image2 f s t
-- Lean.Data.Trie
Lean.Data.Trie.node : {α : Type} → Option α → ByteArray → Array (Lean.Data.Trie α) → Lean.Data.Trie α
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.id_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} (D : F.DescentData f) (i : ι),
  (CategoryTheory.CategoryStruct.id D).hom i = CategoryTheory.CategoryStruct.id (D.obj i)
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- The prelax functor from `Cat` to `Cat` defined with `WithTerminal`.  -/
CategoryTheory.WithTerminal.prelaxfunctor : CategoryTheory.PrelaxFunctor CategoryTheory.Cat CategoryTheory.Cat
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.enrichedId_π_assoc : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ : CategoryTheory.Functor J C)
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₁] (j : J) {Z : V}
  (h : ((CategoryTheory.Enriched.FunctorCategory.diagram V F₁ F₁).obj (Opposite.op j)).obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.enrichedId V F₁)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.end_.π (CategoryTheory.Enriched.FunctorCategory.diagram V F₁ F₁) j) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eId V (F₁.obj j)) h
-- Mathlib.Topology.Separation.Regular
/-- A T₄ space is a normal T₁ space.  -/
T4Space : (X : Type u) → [TopologicalSpace X] → Prop
-- Mathlib.RingTheory.Ideal.Height
_private.Mathlib.RingTheory.Ideal.Height.0.Ideal.height_mono_of_isPrime : ∀ {R : Type u_1} [inst : CommRing R] {I J : Ideal R} [I.IsPrime] [J.IsPrime], I ≤ J → I.height ≤ J.height
-- Init.Data.Slice.Array.Basic
instSliceableArrayNatSubarray_2 : {α : Type u} → Std.Rci.Sliceable (Array α) ℕ (Subarray α)
-- Mathlib.Data.Finsupp.Interval
Finsupp.rangeSingleton_support : ∀ {ι : Type u_1} {α : Type u_2} [inst : Zero α] (f : ι →₀ α), f.rangeSingleton.support = f.support
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedAction_obj_map : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (x : C) {X Y : D} (f : X ⟶ Y),
  ((CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedAction C D).obj x).map f =
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f x
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.symm_mk : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (f : M ≃ N)
  (h : ∀ (x y : M), f.toFun (x + y) = f.toFun x + f.toFun y),
  { toEquiv := f, map_add' := h }.symm = { toEquiv := f.symm, map_add' := ⋯ }
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.HorizontalComp.of.sizeOf_spec : ∀ (η : Mathlib.Tactic.BicategoryLike.WhiskerRight),
  sizeOf (Mathlib.Tactic.BicategoryLike.HorizontalComp.of η) = 1 + sizeOf η
-- Mathlib.Tactic.Determinant.Bird.Cert
/-- The ring tactic normal-form value.  -/
Mathlib.Tactic.Determinant.CertVal : {u : Lean.Level} → {α : Q(Type u)} → Q(CommRing «$α») → Q(«$α») → Type
-- Lean.Parser.Term
Lean.Parser.Term.valueOf.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Group.Submonoid.Finsupp
Submonoid.exists_finsupp_of_mem_closure_range : ∀ {M : Type u_1} [inst : CommMonoid M] {ι : Type u_2} (f : ι → M),
  ∀ x ∈ Submonoid.closure (Set.range f), ∃ a, x = a.prod fun x1 x2 => f x1 ^ x2
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.Functor.isCommMonObj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  {F : CategoryTheory.Functor C D} [inst_6 : F.LaxBraided] {M : C} [inst_7 : CategoryTheory.MonObj M]
  [CategoryTheory.IsCommMonObj M], CategoryTheory.IsCommMonObj (F.obj M)
-- Mathlib.Data.Fin.SuccPred
/-- `succAbove` is injective at the pivot  -/
Fin.succAbove_left_inj : ∀ {n : ℕ} {x y : Fin (n + 1)}, x.succAbove = y.succAbove ↔ x = y
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- The `AddEquiv` between the kernel of the restriction map to a normal subgroup `H` of homomorphisms
of type `G →+ A` and the group of homomorphisms `G ⧸ H →+ A`.
 -/
AddMonoidHom.domRestrictHomKerEquiv : {G : Type u} →
  [inst : AddGroup G] →
    (A : Type u_1) →
      [inst_1 : AddCommGroup A] →
        (H : AddSubgroup G) → [inst_2 : H.Normal] → ↥(AddMonoidHom.domRestrictHom H A).ker ≃+ (G ⧸ H →+ A)
-- Mathlib.Geometry.Euclidean.Triangle
/-- In a triangle, the smaller angle is opposite the smaller side.  -/
EuclideanGeometry.dist_lt_of_angle_lt : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {a b c : P},
  ¬Collinear ℝ {a, b, c} → EuclideanGeometry.angle a c b < EuclideanGeometry.angle a b c → dist a b < dist a c
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.Context.mk.sizeOf_spec : ∀ (config : Lean.Meta.Sym.DSimp.Config), sizeOf { config := config } = 1 + sizeOf config
-- Std.Sat.CNF.Basic
Std.Sat.CNF.Internal.clauses_append : ∀ {α : Type u_1} {f1 f2 : Std.Sat.CNF α}, (f1 ++ f2).clauses = f1.clauses ++ f2.clauses
-- Batteries.Recycling.RBTree.Basic
RBTree.instReprRBNode.repr : {α : Type u_1} → [Repr α] → RBTree.RBNode α → ℕ → Std.Format
-- Init.Data.String.Iterate
String.Slice.PosIterator.mk.injEq : ∀ {s : String.Slice} (currPos currPos_1 : s.Pos),
  ({ currPos := currPos } = { currPos := currPos_1 }) = (currPos = currPos_1)
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.congr'_enorm : ∀ {α : Type u_1} {ε : Type u_5} {ε' : Type u_6} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] [inst_2 : TopologicalSpace ε'] [inst_3 : ContinuousENorm ε']
  {f : α → ε} {g : α → ε'},
  MeasureTheory.Integrable f μ →
    MeasureTheory.AEStronglyMeasurable g μ → (∀ᵐ (a : α) ∂μ, ‖f a‖ₑ = ‖g a‖ₑ) → MeasureTheory.Integrable g μ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.mem_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {f : α → β → Bool} {k : α},
  k ∈ Std.DTreeMap.filter f t ↔ ∃ (h' : k ∈ t), f (t.getKey k h') (Std.DTreeMap.Const.get t k h') = true
-- Mathlib.Algebra.Order.GroupWithZero.Defs
posMulStrictMono_iff_mulPosStrictMono : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [IsMulCommutative α],
  PosMulStrictMono α ↔ MulPosStrictMono α
-- Mathlib.Algebra.Category.Grp.Basic
/-- The type of morphisms in `GrpCat R`.  -/
GrpCat.Hom : GrpCat → GrpCat → Type u
-- Mathlib.CategoryTheory.Subfunctor.Image
CategoryTheory.Subfunctor.fromPreimage_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C (Type w)}
  (G : CategoryTheory.Subfunctor F) (p : F' ⟶ F),
  CategoryTheory.CategoryStruct.comp (G.fromPreimage p) G.ι = CategoryTheory.CategoryStruct.comp (G.preimage p).ι p
-- Qq.Macro
Qq.Impl.quoteExpr : Lean.Expr → Qq.Impl.QuoteM Lean.Expr
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_diff_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ((t₁ \ t₂).isEmpty = true ↔ ∀ k ∈ t₁, k ∈ t₂)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.getₘ_eq_getValueCast : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : Std.LawfulEqOrd α] [inst_3 : BEq α]
  [inst_4 : Std.LawfulBEqOrd α] {k : α} {t : Std.DTreeMap.Internal.Impl α β}
  (h : Std.Internal.List.containsKey k t.toListModel = true) {h' : (t.get?ₘ k).isSome = true},
  t.Ordered → t.getₘ k h' = Std.Internal.List.getValueCast k t.toListModel h
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
CategoryTheory.Limits.WeakLimitCone.mk : {J : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} J] →
    {C : Type u_3} →
      [inst_1 : CategoryTheory.Category.{v_3, u_3} C] →
        {F : CategoryTheory.Functor J C} →
          (cone : CategoryTheory.Limits.Cone F) →
            CategoryTheory.Limits.IsWeakLimit cone → CategoryTheory.Limits.WeakLimitCone F
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.isCocycle₁_of_mem_cocycles₁ : ∀ {k G A : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup A] [inst_3 : Module k A]
  [inst_4 : DistribMulAction G A] [inst_5 : SMulCommClass G k A],
  ∀ f ∈ groupCohomology.cocycles₁ (Rep.ofDistribMulAction k G A), groupCohomology.IsCocycle₁ f
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey_alter : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] [Inhabited α] {k k' : α} (h : (↑m).WF) {f : Option (β k) → Option (β k)}
  (hc : (m.alter k f).contains k' = true),
  (m.alter k f).getKey k' hc = if heq : (k == k') = true then k else m.getKey k' ⋯
-- Mathlib.Algebra.Group.Basic
add_self_zsmul : ∀ {G : Type u_3} [inst : AddGroup G] (a : G) (n : ℤ), n • a + a = (n + 1) • a
-- Mathlib.RepresentationTheory.Coinduced
/-- Given a monoid morphism `φ : G →* H` and a morphism of `G`-representations `f : A ⟶ B`, there
is a natural `H`-representation morphism `coind φ A ⟶ coind φ B`, given by postcomposition by
`f`.  -/
Rep.coindMap : {k : Type u} →
  {G : Type v} →
    {H : Type w} →
      [inst : CommRing k] →
        [inst_1 : Monoid G] →
          [inst_2 : Monoid H] →
            (φ : G →* H) →
              {A B : Rep.{u_1, u, v} k G} → (A ⟶ B) → (Rep.coind.{u, v, w, u_1} φ A ⟶ Rep.coind.{u, v, w, u_1} φ B)
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf_eq_zero : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G}, ¬IsOfFinAddOrder x → addOrderOf x = 0
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
_private.Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution.0.DiscreteConvolution.mulFiber_swapEquiv.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M] (x : M),
  DiscreteConvolution.mulFiber_swapEquiv✝ x =
    {
      toFun := fun x_1 =>
        match x_1 with
        | ⟨p, h⟩ => ⟨p.swap, ⋯⟩,
      invFun := fun x_1 =>
        match x_1 with
        | ⟨p, h⟩ => ⟨p.swap, ⋯⟩,
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.CategoryTheory.Category.Quiv
CategoryTheory.Quiv.hom_obj_inv_obj_of_iso : ∀ {V W : CategoryTheory.Quiv} (e : V ≅ W) (Y : ↑W), e.hom.obj (e.inv.obj Y) = Y
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
IsDecompositionField.mk : ∀ {K : Type u_2} {L : Type u_3} {B : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : CommRing B] {P : Ideal B} {D : Type u_5} [inst_4 : Field D] [inst_5 : Algebra D L]
  [inst_6 : MulSemiringAction Gal(L/K) B] [toIsGaloisGroup : IsGaloisGroup (↥(MulAction.stabilizer Gal(L/K) P)) D L],
  IsDecompositionField K L P D
-- Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Nat.Partition.genFun.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] (f : ℕ → ℕ → R),
  Nat.Partition.genFun f = PowerSeries.mk fun n => ∑ p, (Multiset.toFinsupp p.parts).prod f
-- Mathlib.Topology.Algebra.Star
tendsto_star : ∀ {R : Type u_2} [inst : TopologicalSpace R] [inst_1 : Star R] [ContinuousStar R] (a : R),
  Filter.Tendsto star (nhds a) (nhds (star a))
-- Mathlib.GroupTheory.Index
AddSubgroup.index_iInf_le : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_3} [inst_1 : Fintype ι] (f : ι → AddSubgroup G),
  (⨅ i, f i).index ≤ ∏ i, (f i).index
-- Init.Data.Array.BinSearch
_private.Init.Data.Array.BinSearch.0.Array.binSearchAux.eq_def : ∀ {α : Type u} {β : Type v} (lt : α → α → Bool) (found : Option α → β) (as : Array α) (k : α) (x : Fin (as.size + 1))
  (x_1 : Fin as.size) (x_2 : ↑x ≤ ↑x_1),
  Array.binSearchAux lt found as k x x_1 x_2 =
    match x, x_1, x_2 with
    | lo, hi, h =>
      let m := (↑lo + ↑hi) / 2;
      have a := as[m];
      if lt a k = true then if h' : m + 1 ≤ ↑hi then Array.binSearchAux lt found as k ⟨m + 1, ⋯⟩ hi h' else found none
      else
        if lt k a = true then
          if h' : m = 0 ∨ m - 1 < ↑lo then found none else Array.binSearchAux lt found as k lo ⟨m - 1, ⋯⟩ ⋯
        else found (some a)