mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Congruence.BigOperators
/-- Additive congruence relations preserve finite sum.  -/
AddCon.finsetSum : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] (c : AddCon M) (s : Finset ι) {f g : ι → M},
  (∀ i ∈ s, c (f i) (g i)) → c (s.sum f) (s.sum g)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.get!_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α] {k : α} [inst_3 : Inhabited (β k)], m₁.WF → m₂.WF → m₁.Equiv m₂ → m₁.get! k = m₂.get! k
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k : α}, (Std.ExtTreeMap.filter f t).getKey? k = (t.getKey? k).pfilter fun x h' => f x t[x]
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonPlainGoalParams : Lean.FromJson Lean.Lsp.PlainGoalParams
-- Batteries.Data.List.Basic
List.sections.eq_2 : ∀ {α : Type u_1} (l : List α) (L : List (List α)),
  (l :: L).sections = List.flatMap (fun s => List.map (fun a => a :: s) l) L.sections
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.transpose_add_cbm : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] (μ : MeasureTheory.VectorMeasure X F) (B C : E →L[ℝ] F →L[ℝ] G),
  μ.transpose (B + C) = μ.transpose B + μ.transpose C
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.mem_iff_toUnits_mem_units : ∀ {G : Type u_2} [inst : Group G] (H : Subgroup G) (x : G), toUnits x ∈ H.units ↔ x ∈ H
-- Mathlib.Order.Filter.CountableInter
Filter.EventuallyLE.countable_bUnion : ∀ {α : Type u_2} {l : Filter α} [CountableInterFilter l] {ι : Type u_4} {S : Set ι},
  S.Countable →
    ∀ {s t : (i : ι) → i ∈ S → Set α},
      (∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi) → ⋃ i, ⋃ (h : i ∈ S), s i h ≤ᶠ[l] ⋃ i, ⋃ (h : i ∈ S), t i h
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] [inst_1 : Inhabited α],
  t.WF →
    ∀ {k k' : α} {f : Option (β k) → Option (β k)},
      (t.alter k f).getKey! k' =
        if cmp k k' = Ordering.eq then if (f (t.get? k)).isSome = true then k else default else t.getKey! k'
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.match_1.congr_eq_5 : ∀ (motive : ByteArray.utf8DecodeChar?.FirstByte → Sort u_1) (x : ByteArray.utf8DecodeChar?.FirstByte)
  (h_1 : x = ByteArray.utf8DecodeChar?.FirstByte.invalid → motive ByteArray.utf8DecodeChar?.FirstByte.invalid)
  (h_2 : x = ByteArray.utf8DecodeChar?.FirstByte.done → motive ByteArray.utf8DecodeChar?.FirstByte.done)
  (h_3 : x = ByteArray.utf8DecodeChar?.FirstByte.oneMore → motive ByteArray.utf8DecodeChar?.FirstByte.oneMore)
  (h_4 : x = ByteArray.utf8DecodeChar?.FirstByte.twoMore → motive ByteArray.utf8DecodeChar?.FirstByte.twoMore)
  (h_5 : x = ByteArray.utf8DecodeChar?.FirstByte.threeMore → motive ByteArray.utf8DecodeChar?.FirstByte.threeMore)
  (heq_1 : x = ByteArray.utf8DecodeChar?.FirstByte.threeMore),
  (match h : x with
    | ByteArray.utf8DecodeChar?.FirstByte.invalid => h_1 h
    | ByteArray.utf8DecodeChar?.FirstByte.done => h_2 h
    | ByteArray.utf8DecodeChar?.FirstByte.oneMore => h_3 h
    | ByteArray.utf8DecodeChar?.FirstByte.twoMore => h_4 h
    | ByteArray.utf8DecodeChar?.FirstByte.threeMore => h_5 h) ≍
    h_5 heq_1
-- Batteries.Tactic.PrintOpaques
Batteries.Tactic.CollectOpaques.State.mk.injEq : ∀ (visited : Lean.NameSet) (opaques : Array Lean.Name) (visited_1 : Lean.NameSet) (opaques_1 : Array Lean.Name),
  ({ visited := visited, opaques := opaques } = { visited := visited_1, opaques := opaques_1 }) =
    (visited = visited_1 ∧ opaques = opaques_1)
-- Mathlib.Topology.MetricSpace.GromovHausdorff
/-- In particular, nonempty compacts of a metric space map to `GHSpace`.
We register this in the `TopologicalSpace` namespace to take advantage
of the notation `p.toGHSpace`.  -/
TopologicalSpace.NonemptyCompacts.toGHSpace : {X : Type u} → [inst : MetricSpace X] → TopologicalSpace.NonemptyCompacts X → GromovHausdorff.GHSpace
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.ExtendScalars.hom_ext : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S} {M : ModuleCat R}
  {N : ModuleCat S} {α β : (ModuleCat.extendScalars f).obj M ⟶ N},
  (∀ (m : ↑M),
      (CategoryTheory.ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (CategoryTheory.ConcreteCategory.hom β) (1 ⊗ₜ[R] m)) →
    α = β
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
/-- Merge two `PreDiscrTree`s.  -/
Lean.Meta.RefinedDiscrTree.PreDiscrTree.append : {α : Type} →
  Lean.Meta.RefinedDiscrTree.PreDiscrTree α →
    Lean.Meta.RefinedDiscrTree.PreDiscrTree α → Lean.Meta.RefinedDiscrTree.PreDiscrTree α
-- Batteries.Data.List.Lemmas
List.sum_pair : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Zero α] [Std.LawfulRightIdentity (fun x1 x2 => x1 + x2) 0] {a b : α},
  [a, b].sum = a + b
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
QuadraticModuleCat.ofIso_refl : ∀ {R : Type u} [inst : CommRing R] {X : Type v} [inst_1 : AddCommGroup X] [inst_2 : Module R X]
  {Q₁ : QuadraticForm R X},
  QuadraticModuleCat.ofIso (QuadraticMap.IsometryEquiv.refl Q₁) = CategoryTheory.Iso.refl (QuadraticModuleCat.of Q₁)
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
/-- `Edge.id x` is a composition of `Edge.id x` with `Edge.id x`.  -/
SSet.Truncated.Edge.CompStruct.idCompId : {X : SSet.Truncated 2} →
  (x : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })) →
    (SSet.Truncated.Edge.id x).CompStruct (SSet.Truncated.Edge.id x) (SSet.Truncated.Edge.id x)
-- Init.Data.Int.Linear
Int.Internal.Linear.dvd_solve_elim_cert.eq_1 : ∀ (d₁ d₂ d : ℤ) (p : Int.Internal.Linear.Poly) (a₁ : ℤ) (x₁ : Int.Internal.Linear.Var) (p₁_2 : Int.Internal.Linear.Poly)
  (a₂ : ℤ) (x₂ : Int.Internal.Linear.Var) (p₂_2 : Int.Internal.Linear.Poly),
  Int.Internal.Linear.dvd_solve_elim_cert d₁ (Int.Internal.Linear.Poly.add a₁ x₁ p₁_2) d₂
      (Int.Internal.Linear.Poly.add a₂ x₂ p₂_2) d p =
    (Nat.beq x₁ x₂ &&
      (d.beq' ↑((a₁ * d₂).gcd (a₂ * d₁)) && p.beq' (Int.Internal.Linear.Poly.combine_mul_k a₂ (-a₁) p₁_2 p₂_2)))
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKeyD_insertIfNew_le_minKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    t.isEmpty = false →
      ∀ {k : α} {v : β k} {fallback : α}, (cmp ((t.insertIfNew k v).minKeyD fallback) (t.minKeyD fallback)).isLE = true
-- Mathlib.Algebra.GroupWithZero.Defs
CancelCommMonoidWithZero.mk.injEq : ∀ {M₀ : Type u_2} (toCommMonoidWithZero : CommMonoidWithZero M₀) (toIsLeftCancelMulZero : IsLeftCancelMulZero M₀)
  (toCommMonoidWithZero_1 : CommMonoidWithZero M₀) (toIsLeftCancelMulZero_1 : IsLeftCancelMulZero M₀),
  ({ toCommMonoidWithZero := toCommMonoidWithZero, toIsLeftCancelMulZero := toIsLeftCancelMulZero } =
      { toCommMonoidWithZero := toCommMonoidWithZero_1, toIsLeftCancelMulZero := toIsLeftCancelMulZero_1 }) =
    (toCommMonoidWithZero = toCommMonoidWithZero_1)
-- Init.Data.Array.Sort.Lemmas
Array.mergeSort_singleton : ∀ {α : Type u_1} {r : α → α → Bool} {a : α}, #[a].mergeSort r = #[a]
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The `<` order on subspaces is the same as that on the corresponding sets.  -/
AffineSubspace.lt_def : ∀ {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] (s₁ s₂ : AffineSubspace k P), s₁ < s₂ ↔ ↑s₁ ⊂ ↑s₂
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
ContinuousMap.AlgHom.closure_ker_inter : ∀ {F : Type u_2} {S : Type u_3} {K : Type u_4} {A : Type u_5} [inst : CommRing K] [inst_1 : Ring A]
  [inst_2 : Algebra K A] [inst_3 : TopologicalSpace K] [T1Space K] [inst_5 : TopologicalSpace A] [ContinuousSub A]
  [ContinuousSMul K A] [inst_8 : FunLike F A K] [inst_9 : AlgHomClass F K A K] [inst_10 : SetLike S A] [OneMemClass S A]
  [AddSubgroupClass S A] [SMulMemClass S K A] (φ : F),
  Continuous ⇑φ → ∀ (s : S), closure (↑s ∩ ↑(RingHom.ker φ)) = closure ↑s ∩ ↑(RingHom.ker φ)
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.mapTermRel.eq_1 : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} {β : Type v'} {g : ℕ → ℕ}
  (ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin (g n))) (fr : (n : ℕ) → L.Relations n → L'.Relations n)
  (h : (n : ℕ) → L'.BoundedFormula β (g (n + 1)) → L'.BoundedFormula β (g n + 1)) (x : ℕ),
  FirstOrder.Language.BoundedFormula.mapTermRel ft fr h FirstOrder.Language.BoundedFormula.falsum =
    FirstOrder.Language.BoundedFormula.falsum
-- Init.Data.Int.DivMod.Bootstrap
Int.ediv_mul_cancel_of_emod_eq_zero : ∀ {a b : ℤ}, a % b = 0 → a / b * b = a
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instInv : {G : Type u_1} → [inst : TopologicalSpace G] → [inst_1 : Inv G] → [ContinuousInv G] → Inv (SeparationQuotient G)
-- Mathlib.RingTheory.PowerSeries.Evaluation
PowerSeries.comp_aeval : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {a : S} [inst_2 : UniformSpace R]
  [inst_3 : UniformSpace S] [inst_4 : IsUniformAddGroup R] [inst_5 : IsTopologicalSemiring R]
  [inst_6 : IsUniformAddGroup S] [inst_7 : T2Space S] [inst_8 : CompleteSpace S] [inst_9 : IsTopologicalRing S]
  [inst_10 : IsLinearTopology S S] [inst_11 : Algebra R S] [inst_12 : ContinuousSMul R S] (ha : PowerSeries.HasEval a)
  {T : Type u_3} [inst_13 : CommRing T] [inst_14 : UniformSpace T] [inst_15 : IsUniformAddGroup T]
  [inst_16 : IsTopologicalRing T] [inst_17 : IsLinearTopology T T] [inst_18 : T2Space T] [inst_19 : Algebra R T]
  [inst_20 : ContinuousSMul R T] [inst_21 : CompleteSpace T] {ε : S →ₐ[R] T} (hε : Continuous ⇑ε),
  ε.comp (PowerSeries.aeval ha) = PowerSeries.aeval ⋯
-- Mathlib.Topology.Algebra.UniformConvergence
UniformFun.hasBasis_nhds_one : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : UniformSpace G] [IsUniformGroup G],
  (nhds 1).HasBasis (fun V => V ∈ nhds 1) fun V => {f | ∀ (x : α), f x ∈ V}
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivWithinAt_ofNat : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) (s : Set 𝕜) (n : ℕ) [inst_3 : OfNat F n], HasDerivWithinAt (OfNat.ofNat n) 0 s x
-- Mathlib.Order.Disjoint
codisjoint_comm : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] {a b : α}, Codisjoint a b ↔ Codisjoint b a
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.strictMap_strictMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {E : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} E] (P : CategoryTheory.MorphismProperty C)
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E),
  (P.strictMap F).strictMap G = P.strictMap (F.comp G)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- The `b`-th projection from the pi object over `f` has the form `∏ᶜ f ⟶ f b`.  -/
CategoryTheory.Limits.Pi.π : {β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (f : β → C) → [inst_1 : CategoryTheory.Limits.HasProduct f] → (b : β) → ∏ᶜ f ⟶ f b
-- Mathlib.CategoryTheory.MorphismProperty.WeakFactorizationSystem
CategoryTheory.MorphismProperty.IsWeakFactorizationSystem.mk' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W₁ W₂ : CategoryTheory.MorphismProperty C)
  [W₁.HasFactorization W₂] [W₁.IsStableUnderRetracts] [W₂.IsStableUnderRetracts],
  (∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y), W₁ i → W₂ p → CategoryTheory.HasLiftingProperty i p) →
    W₁.IsWeakFactorizationSystem W₂
-- Std.Data.ExtTreeMap.Basic
Std.ExtTreeMap.instForMProdOfTransCmpOfLawfulMonad : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      {m : Type w → Type w₂} →
        [Std.TransCmp cmp] → [inst : Monad m] → [LawfulMonad m] → ForM m (Std.ExtTreeMap α β cmp) (α × β)
-- Mathlib.GroupTheory.PGroup
isPGroup_iff_exponent_eq_pow : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [Finite G] [Fact (Nat.Prime p)], IsPGroup p G ↔ ∃ n, Monoid.exponent G = p ^ n
-- Mathlib.Probability.Independence.Integration
/-- If a random variable `X` is independent of a sigma-algebra `m` and `A` is a set in `m`
then `∫ ω in A, f (X ω) ∂P = P.real A • ∫ ω, f (X ω) ∂P` for a measurable function `f : 𝓧 → E`.  -/
ProbabilityTheory.Indep.setIntegral_eq_smul : ∀ {Ω : Type u_5} {𝓧 : Type u_6} {m mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [m𝓧 : MeasurableSpace 𝓧]
  {X : Ω → 𝓧} {A : Set Ω} {E : Type u_7} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E],
  m ≤ mΩ →
    ∀ {f : 𝓧 → E},
      ProbabilityTheory.Indep m (MeasurableSpace.comap X m𝓧) P →
        AEMeasurable X P →
          MeasurableSet A →
            MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map X P) →
              ∫ (ω : Ω) in A, f (X ω) ∂P = P.real A • ∫ (ω : Ω), f (X ω) ∂P
-- Mathlib.Computability.PartrecCode
/-- A modified evaluation for the code which returns an `Option ℕ` instead of a `Part ℕ`. To avoid
undecidability, `evaln` takes a parameter `k` and fails if it encounters a number ≥ k in the course
of its execution. Other than this, the semantics are the same as in `Nat.Partrec.Code.eval`.
 -/
Nat.Partrec.Code.evaln : ℕ → Nat.Partrec.Code → ℕ → Option ℕ
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.dvd_iterate_derivative_pow : ∀ {R : Type u} [inst : CommSemiring R] (f : Polynomial R) (n : ℕ) {m : ℕ} (c : R),
  m ≠ 0 → ↑n ∣ Polynomial.eval c ((⇑Polynomial.derivative)^[m] (f ^ n))
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
SSet.Nonsingular.δ_injective : ∀ {X : SSet} [X.Nonsingular] {n : ℕ},
  ∀ x ∈ X.nonDegenerate (n + 1),
    ∀ (i j : Fin (n + 2)),
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X i)) x =
          (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X j)) x →
        i = j
-- Init.Meta.Defs
Lean.Syntax.findAux : (Lean.Syntax → Bool) → Lean.Syntax → Option Lean.Syntax
-- Mathlib.RingTheory.Polynomial.HilbertPoly
Polynomial.preHilbertPoly_eq_choose_sub_add : ∀ (F : Type u_1) [inst : Field F] [CharZero F] (d : ℕ) {k n : ℕ},
  k ≤ n → Polynomial.eval (↑n) (Polynomial.preHilbertPoly F d k) = ↑((n - k + d).choose d)
-- Std.Data.Internal.List.Associative
Std.Internal.List.foldr_eq_foldr_toProd : ∀ {α : Type u} {β : Type v} {δ : Type w} {l : List ((_ : α) × β)} {f : α → β → δ → δ} {init : δ},
  List.foldr (fun a b => f a.fst a.snd b) init l =
    List.foldr (fun a b => f a.1 a.2 b) init (List.map (fun x => (x.fst, x.snd)) l)
-- Mathlib.Algebra.Ring.Subring.Basic
/-- Given `Subring`s `s`, `t` of rings `R`, `S` respectively, `s.prod t` is `s ×̂ t`
as a subring of `R × S`.  -/
Subring.prod : {R : Type u} →
  {S : Type v} → [inst : NonAssocRing R] → [inst_1 : NonAssocRing S] → Subring R → Subring S → Subring (R × S)
-- Init.Data.Order.Lemmas
Std.le_antisymm_iff : ∀ {α : Type u} [inst : LE α] [Std.Antisymm fun x1 x2 => x1 ≤ x2] [Std.Refl fun x1 x2 => x1 ≤ x2] {a b : α},
  a ≤ b ∧ b ≤ a ↔ a = b
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.mk : {𝕜 : Type u_4} →
  {F : Type u_5} →
    [inst : RCLike 𝕜] →
      [inst_1 : AddCommGroup F] →
        [inst_2 : Module 𝕜 F] →
          (toCore : PreInnerProductSpace.Core 𝕜 F) → (∀ (x : F), inner 𝕜 x x = 0 → x = 0) → InnerProductSpace.Core 𝕜 F
-- Mathlib.Tactic.NormNum.LegendreSymbol
Mathlib.Meta.NormNum.jacobiSymNat.qr₃_mod : ∀ (a b ab : ℕ) (r : ℤ),
  a % 4 = 3 →
    b % 4 = 3 → b % a = ab → Mathlib.Meta.NormNum.jacobiSymNat ab a = r → Mathlib.Meta.NormNum.jacobiSymNat a b = -r
-- Mathlib.MeasureTheory.Measure.Regular
/-- The restriction of a regular measure to a set of finite measure is regular.  -/
MeasureTheory.Measure.Regular.restrict_of_measure_ne_top : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α] [R1Space α]
  [BorelSpace α] [μ.Regular] {A : Set α}, μ A ≠ ⊤ → (μ.restrict A).Regular
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_of_mem_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k a : α}, a ∈ t.erase k → a ∈ t
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.distribMulAction : {R : Type u_1} →
  {S : Type u_2} →
    {M : Type u_3} →
      [inst : Monoid S] → [inst_1 : Semiring R] → [DistribMulAction S R] → DistribMulAction S (MonoidAlgebra R M)
-- Mathlib.Data.Nat.Bits
Nat.shiftLeft'_add : ∀ (b : Bool) (m n k : ℕ), Nat.shiftLeft' b m (n + k) = Nat.shiftLeft' b (Nat.shiftLeft' b m n) k
-- Mathlib.LinearAlgebra.Prod
LinearEquiv.coe_uniqueProd : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] [inst_5 : Unique M₂], ↑LinearEquiv.uniqueProd = Equiv.uniqueProd M M₂
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Mon.denote.match_1.eq_2 : ∀ (motive : Lean.Grind.CommRing.Mon → Sort u_1) (p : Lean.Grind.CommRing.Power) (m : Lean.Grind.CommRing.Mon)
  (h_1 : Unit → motive Lean.Grind.CommRing.Mon.unit)
  (h_2 : (p : Lean.Grind.CommRing.Power) → (m : Lean.Grind.CommRing.Mon) → motive (Lean.Grind.CommRing.Mon.mult p m)),
  (match Lean.Grind.CommRing.Mon.mult p m with
    | Lean.Grind.CommRing.Mon.unit => h_1 ()
    | Lean.Grind.CommRing.Mon.mult p m => h_2 p m) =
    h_2 p m
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.instNeg : {𝕜 : 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} →
                {G : Type u_4} →
                  [inst_4 : TopologicalSpace G] →
                    [inst_5 : ChartedSpace H G] →
                      [inst_6 : Monoid G] → [inst_7 : ContMDiffMul I (↑⊤) G] → Neg (LeftInvariantDerivation I G)
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.HasGaussianLaw.charFun_map_eq : ∀ {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : MeasurableSpace E] [BorelSpace E] {X : Ω → E} [inst_3 : InnerProductSpace ℝ E] (t : E),
  ProbabilityTheory.HasGaussianLaw X P →
    MeasureTheory.charFun (MeasureTheory.Measure.map X P) t =
      Complex.exp
        (↑(∫ (x : Ω), (fun ω => inner ℝ t (X ω)) x ∂P) * Complex.I -
          ↑(ProbabilityTheory.variance (fun ω => inner ℝ t (X ω)) P) / 2)
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
LinearIndependent.pair_add_right_iff : ∀ {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x y : M},
  LinearIndependent R ![x, x + y] ↔ LinearIndependent R ![x, y]
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.Equiv.ext : ∀ {α : Type u} {s t : Stream'.WSeq α}, (∀ (n : ℕ), (s.get? n).Equiv (t.get? n)) → s ~ʷ t
-- Init.Data.UInt.Lemmas
UInt32.toBitVec_toUInt16 : ∀ (n : UInt32), n.toUInt16.toBitVec = BitVec.setWidth 16 n.toBitVec
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.length_cons : ∀ {V : Type u} [inst : Quiver V] (a b c : V) (p : Quiver.Path a b) (e : b ⟶ c), (p.cons e).length = p.length + 1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.π_iso_of_iso_right_hom : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} {f₁ : CategoryTheory.Arrow C₁}
  {f₃ f₃' : CategoryTheory.Arrow C₃} (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) (sq₁₃' : G.PullbackObjObj f₁.hom f₃'.hom)
  (iso : f₃ ≅ f₃'), (sq₁₃.π_iso_of_iso_right sq₁₃' iso).hom = sq₁₃.mapArrowRight sq₁₃' iso.hom
-- Mathlib.Order.WellFoundedSet
Set.wellFoundedOn_iff : ∀ {α : Type u_2} {r : α → α → Prop} {s : Set α}, s.WellFoundedOn r ↔ WellFounded fun a b => r a b ∧ a ∈ s ∧ b ∈ s
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.b₆_of_char_two : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [CharP R 2], W.b₆ = W.a₃ ^ 2
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.AbsolutelyContinuous.compProd_right : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ η : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite μ] [ProbabilityTheory.IsSFiniteKernel η],
  (∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a)) → (μ.compProd κ).AbsolutelyContinuous (μ.compProd η)
-- Init.Data.String.Lemmas.Order
String.Pos.not_lt_startPos : ∀ {s : String} {p : s.Pos}, ¬p < s.startPos
-- Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
EuclideanSpace.volume_ball_fin_two : ∀ (x : EuclideanSpace ℝ (Fin 2)) (r : ℝ),
  MeasureTheory.volume (Metric.ball x r) = ENNReal.ofReal r ^ 2 * ENNReal.ofReal Real.pi
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.unbotD_one : ∀ {α : Type u} [inst : One α] (d : α), WithBot.unbotD d 1 = 1
-- Mathlib.AlgebraicTopology.SimplicialSet.Dimension
SSet.Subcomplex.le_iff_of_hasDimensionLT : ∀ {X : SSet} (A B : X.Subcomplex) (d : ℕ) [X.HasDimensionLT d],
  A ≤ B ↔ ∀ i < d, A.obj (Opposite.op { len := i }) ∩ X.nonDegenerate i ⊆ B.obj (Opposite.op { len := i })
-- Mathlib.LinearAlgebra.Matrix.HadamardMatrix
Matrix.IsHadamard.apply_mem : ∀ {n : Type u_2} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R] [inst_3 : StarRing R]
  {A : Matrix n n R}, A.IsHadamard → ∀ (i j : n), A i j ∈ unitary R
-- Mathlib.Algebra.Homology.Factorizations.CM5a
/-- The single complex in degree `n₁` that is given by an injective
object containing `K.opcycles n₁`.  -/
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.S : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      CochainComplex C ℤ → [CategoryTheory.EnoughInjectives C] → ℤ → CochainComplex C ℤ
-- Mathlib.Data.Prod.TProd
List.TProd.mk.eq_def : ∀ {ι : Type u} {α : ι → Type v} (x : List ι),
  List.TProd.mk x =
    match (motive := (x : List ι) → ((i : ι) → α i) → List.TProd α x) x with
    | [] => fun x => PUnit.unit
    | i :: is => fun f => (f i, List.TProd.mk is f)
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.weightedDecomposition.decompose'_apply : ∀ (R : Type u_1) {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} (w : σ → M) [inst_1 : AddCommMonoid M]
  [inst_2 : DecidableEq M] (φ : MvPolynomial σ R) (m : M),
  ↑((DirectSum.Decomposition.decompose' φ) m) = (MvPolynomial.weightedHomogeneousComponent w m) φ
-- Std.Sat.AIG.Cached
/-- A version of `AIG.mkConst` that uses the subterm cache in `AIG`. This version is meant for
programming, for proving purposes use `AIG.mkGate` and equality theorems to this one.
 -/
Std.Sat.AIG.mkConstCached : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → (aig : Std.Sat.AIG α) → Bool → aig.Ref
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.Struct.ofNatZero : Lean.Meta.Grind.Arith.Linear.Struct → Lean.Expr
-- Mathlib.Algebra.Category.CommBialgCat
commBialgCatEquivComonCommAlgCat_counitIso_hom_app : ∀ (R : Type u) [inst : CommRing R] (X : (CategoryTheory.Mon (CommAlgCat R)ᵒᵖ)ᵒᵖ),
  (commBialgCatEquivComonCommAlgCat R).counitIso.hom.app X =
    CategoryTheory.CategoryStruct.id
      (Opposite.op
        { X := Opposite.op (CommAlgCat.of R ↑(Opposite.unop (Opposite.unop X).X)), mon := CommAlgCat.monObjOpOf })