mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
ContMDiff.mdifferentiable : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {n : WithTop ℕ∞},
  ContMDiff I I' n f → n ≠ 0 → MDiff f
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.head?_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Min α] [inst_2 : LE α] [Std.LawfulOrderCmp cmp] [Std.LawfulOrderMin α] [Std.LawfulOrderLeftLeaningMin α]
  [Std.LawfulEqCmp cmp], t.keys.head? = t.minKey?
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- Format the application `f args`.  -/
Lean.Meta.RefinedDiscrTree.keysAsPattern.mkApp : Array Lean.Meta.RefinedDiscrTree.Key →
  Lean.MessageData →
    ℕ → Bool → StateRefT' IO.RealWorld (List Lean.Meta.RefinedDiscrTree.Key) Lean.CoreM Lean.MessageData
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.toCotangent_eq : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R) {x y : ↥I}, I.toCotangent x = I.toCotangent y ↔ ↑x - ↑y ∈ I ^ 2
-- Mathlib.NumberTheory.LSeries.RiemannZeta
/-- Alternate formulation of `zeta_eq_tsum_one_div_nat_cpow` with a `+ 1` (to avoid relying
on mathlib's conventions for `0 ^ s`).  -/
zeta_eq_tsum_one_div_nat_add_one_cpow : ∀ {s : ℂ}, 1 < s.re → riemannZeta s = ∑' (n : ℕ), 1 / (↑n + 1) ^ s
-- Mathlib.Algebra.Group.Units.Defs
Units.mk.congr_simp : ∀ {α : Type u} [inst : Monoid α] (val val_1 : α) (e_val : val = val_1) (inv inv_1 : α) (e_inv : inv = inv_1)
  (val_inv : val * inv = 1) (inv_val : inv * val = 1),
  { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val } =
    { val := val_1, inv := inv_1, val_inv := ⋯, inv_val := ⋯ }
-- Init.Data.Iterators.Lemmas.Producers.Monadic.List
List.toListRev_iterM : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} [LawfulMonad m] {l : List β},
  (l.iterM m).toListRev = pure l.reverse
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
CategoryTheory.ObjectProperty.unop_isoClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty Cᵒᵖ),
  P.isoClosure.unop = P.unop.isoClosure
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.instMul : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} → {P : Type u_2} → [inst_1 : CommRing P] → [inst_2 : Algebra R P] → Mul (FractionalIdeal S P)
-- Mathlib.MeasureTheory.MeasurableSpace.Instances
Prop.instMeasurableSingletonClass : MeasurableSingletonClass Prop
-- Mathlib.Data.Nat.Digits.Lemmas
Nat.ofDigits_modEq : ∀ (b k : ℕ) (L : List ℕ), Nat.ofDigits b L ≡ Nat.ofDigits (b % k) L [MOD k]
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec32_or : ∀ (a b : ISize) (h : System.Platform.numBits = 32), (a ||| b).toBitVec32 h = a.toBitVec32 h ||| b.toBitVec32 h
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKey!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) [inst_1 : Inhabited α],
  Std.DTreeMap.Internal.Impl.leaf.getKey! k =
    panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.getKey!" 186 13
      "Key is not present in map"
-- Lean.Compiler.IR.Basic
Lean.IR.Index : Type
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
AlgHom.eqOn_sup : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] {F : Type u_4} [inst_5 : FunLike F A B] [AlgHomClass F R A B] {φ ψ : F}
  {S T : Subalgebra R A}, Set.EqOn ⇑φ ⇑ψ ↑S → Set.EqOn ⇑φ ⇑ψ ↑T → Set.EqOn ⇑φ ⇑ψ ↑(S ⊔ T)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackSymmetry.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPullback f g],
  CategoryTheory.Limits.pullbackSymmetry f g =
    (CategoryTheory.Limits.PullbackCone.flipIsLimit
          (CategoryTheory.Limits.pullbackIsPullback f g)).conePointUniqueUpToIso
      (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Limits.cospan g f))
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.fst_comp_inl : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W},
  (Representation.IntertwiningMap.fst A ρ σ).comp (Representation.IntertwiningMap.inl A ρ σ) =
    Representation.IntertwiningMap.id ρ
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.lift₃_p₃_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Full] {A₁ A₂ A₃ : C} {X : D} {f₁ : F.obj A₁ ⟶ X}
  (hf₁ : F.relativelyRepresentable f₁) (f₂ : F.obj A₂ ⟶ X) (f₃ : F.obj A₃ ⟶ X)
  [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)] [inst_4 : F.Faithful] {Z : C} (x₁ : Z ⟶ A₁)
  (x₂ : Z ⟶ A₂) (x₃ : Z ⟶ A₃)
  (h₁₂ : CategoryTheory.CategoryStruct.comp (F.map x₁) f₁ = CategoryTheory.CategoryStruct.comp (F.map x₂) f₂)
  (h₁₃ : CategoryTheory.CategoryStruct.comp (F.map x₁) f₁ = CategoryTheory.CategoryStruct.comp (F.map x₃) f₃) {Z_1 : C}
  (h : A₃ ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (hf₁.lift₃ f₂ f₃ x₁ x₂ x₃ h₁₂ h₁₃)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₃ hf₁ f₂ f₃) h) =
    CategoryTheory.CategoryStruct.comp x₃ h
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cocycle.rightShift.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (γ γ_1 : CochainComplex.HomComplex.Cocycle K L n),
  γ = γ_1 → ∀ (a n' : ℤ) (hn' : n' + a = n), γ.rightShift a n' hn' = γ_1.rightShift a n' hn'
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get_diff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {h_mem : k ∈ m₁ \ m₂}, (m₁ \ m₂).get k h_mem = m₁.get k ⋯
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.closure_empty : ∀ {G : Type u_1} [inst : AddGroup G], AddSubgroup.closure ∅ = ⊥
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- Restriction of a semigroup hom to its range interpreted as a subsemigroup.  -/
MulHom.srangeRestrict : {M : Type u_1} → [inst : Mul M] → {N : Type u_5} → [inst_1 : Mul N] → (f : M →ₙ* N) → M →ₙ* ↥f.srange
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.add.sizeOf_spec : ∀ (k : ℤ) (v : Lean.Grind.Linarith.Var) (p : Lean.Grind.Linarith.Poly),
  sizeOf (Lean.Grind.Linarith.Poly.add k v p) = 1 + sizeOf k + sizeOf v + sizeOf p
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balanceₘ.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (l : Std.DTreeMap.Internal.Impl α β)
  (motive : (r : Std.DTreeMap.Internal.Impl α β) → r.size > Std.DTreeMap.Internal.delta * l.size → Sort u_3)
  (h : Std.DTreeMap.Internal.Impl.leaf.size > Std.DTreeMap.Internal.delta * l.size)
  (h_1 :
    (h : Std.DTreeMap.Internal.Impl.leaf.size > Std.DTreeMap.Internal.delta * l.size) →
      motive Std.DTreeMap.Internal.Impl.leaf h)
  (h_2 :
    (size : ℕ) →
      (rk : α) →
        (rv : β rk) →
          (rl rr : Std.DTreeMap.Internal.Impl α β) →
            (h : (Std.DTreeMap.Internal.Impl.inner size rk rv rl rr).size > Std.DTreeMap.Internal.delta * l.size) →
              motive (Std.DTreeMap.Internal.Impl.inner size rk rv rl rr) h),
  (match Std.DTreeMap.Internal.Impl.leaf, h with
    | Std.DTreeMap.Internal.Impl.leaf, h => h_1 h
    | Std.DTreeMap.Internal.Impl.inner size rk rv rl rr, h => h_2 size rk rv rl rr h) =
    h_1 h
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
QuasispectrumRestricts.of_quasispectrum_eq : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : Semifield R] [inst_1 : Field S] [inst_2 : NonUnitalRing A]
  [inst_3 : Module R A] [inst_4 : Module S A] [inst_5 : Algebra R S] {a b : A} {f : S → R},
  QuasispectrumRestricts a f → quasispectrum S a = quasispectrum S b → QuasispectrumRestricts b f
-- Init.Data.List.Lemmas
List.getLast_append_left : ∀ {α : Type u_1} {l' l : List α} (w : l ++ l' ≠ []) (h : l' = []), (l ++ l').getLast w = l.getLast ⋯
-- Mathlib.Algebra.Order.Interval.Multiset
Multiset.map_add_left_Icc : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α]
  [inst_4 : LocallyFiniteOrder α] (a b c : α),
  Multiset.map (fun x => c + x) (Multiset.Icc a b) = Multiset.Icc (c + a) (c + b)
-- Mathlib.RingTheory.OreLocalization.OreSet
/-- In rings without zero divisors, the first (cancellability) condition is always fulfilled,
it suffices to give a proof for the Ore condition itself.  -/
OreLocalization.oreSetOfNoZeroDivisors : {R : Type u_1} →
  [inst : Ring R] →
    [NoZeroDivisors R] →
      {S : Submonoid R} →
        (oreNum : R → ↥S → R) →
          (oreDenom : R → ↥S → ↥S) →
            (∀ (r : R) (s : ↥S), ↑(oreDenom r s) * r = oreNum r s * ↑s) → OreLocalization.OreSet S
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wfImp_insertₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m → ∀ {a : α} {b : β a}, Std.DHashMap.Internal.Raw.WFImp ↑(m.insertₘ a b)
-- Mathlib.RingTheory.Teichmuller
Perfection.teichmullerAux.eq_1 : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommRing R] {I : Ideal R} [inst_2 : CharP (R ⧸ I) p]
  (x : Perfection (R ⧸ I) p), x.teichmullerAux 0 = 1
-- Mathlib.Algebra.Group.Prod
MulEquiv.coe_prodComm : ∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N], ⇑MulEquiv.prodComm = Prod.swap
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
/-- A morphism of locally ringed spaces as a morphism of sheafed spaces.  -/
AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom : {X Y : AlgebraicGeometry.LocallyRingedSpace} → X.Hom Y → (X.toSheafedSpace ⟶ Y.toSheafedSpace)
-- Mathlib.Order.Filter.Interval
Filter.tendsto_Ioo_pure_bot : ∀ {α : Type u_1} [inst : PartialOrder α] {a : α}, Filter.TendstoIxxClass Set.Ioo (pure a) ⊥
-- Init.Data.Nat.Control
/-- Iterates the application of a monadic function `f` to a starting value `init`, `n` times. At each
step, `f` is applied to the current value and to the next natural number less than `n`, in
increasing order.
 -/
Nat.foldM : {α : Type u} → {m : Type u → Type v} → [Monad m] → (n : ℕ) → ((i : ℕ) → i < n → α → m α) → α → m α
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.mk_ofAlgEquiv_symm : ∀ {S : Type u_5} [inst : CommRing S] (I : Ideal S) [inst_1 : IsAdicComplete I S] (n : ℕ) (x : AdicCompletion I S),
  (Ideal.Quotient.mk (I ^ n)) ((AdicCompletion.ofAlgEquiv I).symm x) = (AdicCompletion.evalₐ I n) x
-- Mathlib.Algebra.Star.StarRingHom
NonUnitalStarRingHom.instInhabited : {A : Type u_1} →
  {B : Type u_2} →
    [inst : NonUnitalNonAssocSemiring A] →
      [inst_1 : StarAddMonoid A] →
        [inst_2 : NonUnitalNonAssocSemiring B] → [inst_3 : StarAddMonoid B] → Inhabited (A →⋆ₙ+* B)
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.ext_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} {f g : CauSeq β abv}, f = g ↔ ∀ (i : ℕ), ↑f i = ↑g i
-- Mathlib.ModelTheory.Order
FirstOrder.Language.order.instHomClassOfOrderHomClass : ∀ {M : Type w'} [inst : FirstOrder.Language.order.Structure M] [inst_1 : LE M]
  [FirstOrder.Language.order.OrderedStructure M] {N : Type u_1} [inst_3 : FirstOrder.Language.order.Structure N]
  [inst_4 : LE N] [FirstOrder.Language.order.OrderedStructure N] {F : Type u_2} [inst_6 : FunLike F M N]
  [OrderHomClass F M N], FirstOrder.Language.order.HomClass F M N
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.id_mapAddMon_add : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.AddMon C),
  CategoryTheory.AddMonObj.add =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X X.X))
      CategoryTheory.AddMonObj.add
-- Mathlib.Algebra.Polynomial.Mirror
Polynomial.irreducible_of_mirror : ∀ {R : Type u_1} [inst : CommRing R] [NoZeroDivisors R] {f : Polynomial R},
  ¬IsUnit f →
    (∀ (k : Polynomial R), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror) →
      IsRelPrime f f.mirror → Irreducible f
-- Mathlib.Order.Filter.Map
Filter.le_comap_top : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (l : Filter α), l ≤ Filter.comap f ⊤
-- Mathlib.Data.Fintype.Powerset
Finset.filter_subset_univ : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (s : Finset α), {t | t ⊆ s} = s.powerset
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Cfg.mk.sizeOf_spec : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : SizeOf K] [inst_1 : (a : K) → SizeOf (Γ a)]
  [inst_2 : SizeOf Λ] [inst_3 : SizeOf σ] (l : Option Λ) (var : σ) (stk : (k : K) → List (Γ k)),
  sizeOf { l := l, var := var, stk := stk } = 1 + sizeOf l + sizeOf var
-- Mathlib.MeasureTheory.Measure.Restrict
IsCountablySpanning.null_of_forall_restrict_null : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {C : Set (Set α)},
  IsCountablySpanning C → (∀ t ∈ C, MeasurableSet t) → (∀ t ∈ C, (μ.restrict t) s = 0) → μ s = 0
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.splits_next : ∀ {s : String.Slice} (p : s.Pos) (hp : p ≠ s.endPos),
  (p.next hp).Splits ((s.sliceTo p).copy ++ String.singleton (p.get hp)) (s.sliceFrom (p.next hp)).copy
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` reflects colimits of shape `Jᵒᵖ`, then `F.unop : C ⥤ D` reflects limits of
shape `J`.  -/
CategoryTheory.Limits.reflectsLimitsOfShape_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ)
  [CategoryTheory.Limits.ReflectsColimitsOfShape Jᵒᵖ F], CategoryTheory.Limits.ReflectsLimitsOfShape J F.unop
-- Mathlib.RingTheory.RegularLocalRing.Defs
IsRegularLocalRing.of_isRegularRing_of_isLocalRing : ∀ (R : Type u_1) [inst : CommRing R] [IsLocalRing R] [IsRegularRing R], IsRegularLocalRing R
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.expandIfNecessary.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DHashMap.Internal.Raw₀ α β → Sort u_3) →
      (m : Std.DHashMap.Internal.Raw₀ α β) →
        ((size : ℕ) →
            (buckets : Array (Std.DHashMap.Internal.AssocList α β)) →
              (hm : 0 < { size := size, buckets := buckets }.buckets.size) →
                motive ⟨{ size := size, buckets := buckets }, hm⟩) →
          motive m
-- Aesop.Frontend.Tactic
_private.Aesop.Frontend.Tactic.0.Aesop.Frontend.elabSimpConfigCtx.unsafe_1 : Lean.Syntax → Lean.Elab.TermElabM Lean.Meta.Simp.ConfigCtx
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.uniformEquiv_mk_coe : ∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] (a : α ≃ β)
  (b : UniformContinuous a.toFun) (c : UniformContinuous a.invFun),
  ⇑{ toEquiv := a, uniformContinuous_toFun := b, uniformContinuous_invFun := c } = ⇑a
-- Mathlib.LinearAlgebra.Pi
LinearMap.coe_proj : ∀ {R : Type u} {ι : Type x} [inst : Semiring R] {φ : ι → Type i} [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] (i : ι), ⇑(LinearMap.proj i) = Function.eval i
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!_eq_default : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {a : α} [inst_1 : Inhabited (β a)], a ∉ t → t.get! a = default
-- Mathlib.Data.Fin.Init
Fin.xor_assoc : ∀ {n k : ℕ}, k = 2 ^ n → ∀ (a b c : Fin k), a ^^^ b ^^^ c = a ^^^ (b ^^^ c)
-- Mathlib.Topology.Algebra.Monoid.Defs
ContinuousAt.const_add : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Add M] [SeparatelyContinuousAdd M] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f : X → M} {x : X}, ContinuousAt f x → ∀ (b : M), ContinuousAt (fun x => b + f x) x
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.cone_pt : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
  [inst_1 : CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }],
  (CategoryTheory.Limits.Pi.cone X).pt = ∏ᶜ fun j => X.obj { as := j }
-- Init.Data.List.Zip
List.unzip_snd : ∀ {α : Type u_1} {β : Type u_2} {l : List (α × β)}, l.unzip.2 = List.map Prod.snd l
-- Init.Data.List.Control
_private.Init.Data.List.Control.0.List.foldlM.match_1.eq_1 : ∀ {m : Type u_3 → Type u_4} {s : Type u_3} {α : Type u_1} (motive : (s → α → m s) → s → List α → Sort u_2)
  (x : s → α → m s) (s_1 : s) (h_1 : (x : s → α → m s) → (s : s) → motive x s [])
  (h_2 : (f : s → α → m s) → (s : s) → (a : α) → (as : List α) → motive f s (a :: as)),
  (match x, s_1, [] with
    | x, s, [] => h_1 x s
    | f, s, a :: as => h_2 f s a as) =
    h_1 x s_1
-- Init.Data.SInt.Bitwise
Int16.shiftLeft_xor : ∀ {a b c : Int16}, (a ^^^ b) <<< c = a <<< c ^^^ b <<< c
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.toList_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.toList = t₂.toList
-- Mathlib.Data.Real.Basic
Real.instAddCommGroup : AddCommGroup ℝ
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.deleteMin_fst : ∀ {α : Type u_1} {s : Batteries.PairingHeapImp.Heap α} {le : α → α → Bool},
  Option.map (fun x => x.1) (Batteries.PairingHeapImp.Heap.deleteMin le s) = s.head?
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.isScalarTower_right : ∀ {α : Type u_1} {K : Type u_2} [inst : Semiring K] [inst_1 : DistribSMul α K] [IsScalarTower α K K],
  IsScalarTower α (Polynomial K) (Polynomial K)
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
/-- If `‖(1 : β)‖ = 1`, then `‖(1 : α →ᵇ β)‖ = 1` if `α` is nonempty.  -/
BoundedContinuousFunction.instNormOneClass : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β] [Nonempty α]
  [inst_3 : One β] [NormOneClass β], NormOneClass (BoundedContinuousFunction α β)
-- Mathlib.Order.OrderDual
OrderDual.ofDual_symm_eq : ∀ {α : Type u_1}, OrderDual.ofDual.symm = OrderDual.toDual
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α}, (m₁ ∩ m₂).get? k = if k ∈ m₂ then m₁.get? k else none
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.mem_carrier : ∀ {M : Type u_1} [inst : MulOneClass M] {s : Submonoid M} {x : M}, x ∈ s.carrier ↔ x ∈ s
-- Lean.Meta.Canonicalizer
Lean.Meta.Canonicalizer.ExprVisited.e : Lean.Meta.Canonicalizer.ExprVisited → Lean.Expr
-- Mathlib.Tactic.ClickSuggestions.GRewrite
Mathlib.Tactic.ClickSuggestions.GrwPos.mk.inj : ∀ {relName : Lean.Name} {relation : Lean.Expr} {symm? : Option Bool} {relName_1 : Lean.Name} {relation_1 : Lean.Expr}
  {symm?_1 : Option Bool},
  { relName := relName, relation := relation, symm? := symm? } =
      { relName := relName_1, relation := relation_1, symm? := symm?_1 } →
    relName = relName_1 ∧ relation = relation_1 ∧ symm? = symm?_1
-- Mathlib.Algebra.Group.Finsupp
Finsupp.mapRange.addMonoidHom_id : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M],
  Finsupp.mapRange.addMonoidHom (AddMonoidHom.id M) = AddMonoidHom.id (ι →₀ M)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift.0.Std.IterM.toArray_eq_match_step.match_1.eq_3 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3)
  (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
/-- Given a family of measures `μ : (n : ℕ) → Measure (Π i : Iic n, X i)`, the induced family
will be projective only if `μ` is projective, in the sense that if `a ≤ b`, then projecting
`μ b` gives `μ a`.  -/
MeasureTheory.isProjectiveMeasureFamily_inducedFamily : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  (μ : (n : ℕ) → MeasureTheory.Measure ((i : ↥(Finset.Iic n)) → X ↑i)),
  (∀ (a b : ℕ) (hab : a ≤ b), MeasureTheory.Measure.map (Preorder.frestrictLe₂ hab) (μ b) = μ a) →
    MeasureTheory.IsProjectiveMeasureFamily (MeasureTheory.inducedFamily μ)
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.toGenerators : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Algebra.Presentation R S ι σ → Algebra.Generators R S ι
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
CategoryTheory.WideSubcategory.leftUnitor_def : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.MorphismProperty C)
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : P.IsMonoidalStable] (x : CategoryTheory.WideSubcategory P),
  CategoryTheory.MonoidalCategoryStruct.leftUnitor x =
    CategoryTheory.WideSubcategory.isoMk (CategoryTheory.MonoidalCategoryStruct.leftUnitor x.obj) ⋯ ⋯
-- Mathlib.Algebra.Order.Archimedean.Basic
instArchimedeanNat : Archimedean ℕ
-- Init.Data.Array.Zip
Array.zipWith_foldr_eq_zip_foldr : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {as : Array α} {bs : Array β} {g : γ → δ → δ}
  {f : α → β → γ} {i : δ},
  Array.foldr g i (Array.zipWith f as bs) = Array.foldr (fun p r => g (f p.1 p.2) r) i (as.zip bs)
-- Lean.Compiler.ExternAttr
/-- Call to a Lean function without exported IR.  -/
Lean.ExternEntry.opaque : Lean.ExternEntry
-- Init.Data.Fin.Lemmas
Fin.castLE_refl : ∀ {n : ℕ} (h : n ≤ n) (i : Fin n), Fin.castLE h i = i
-- Mathlib.Order.SuccPred.Limit
IsGLB.mem_of_not_isPredPrelimit : ∀ {α : Type u_1} {a : α} [inst : LinearOrder α] {s : Set α}, IsGLB s a → ¬Order.IsPredPrelimit a → a ∈ s
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.instLinearOrderValueGroupWithZero : {R : Type u_1} → [inst : Semiring R] → [inst_1 : ValuativeRel R] → LinearOrder (ValuativeRel.ValueGroupWithZero R)
-- Mathlib.Order.Birkhoff
OrderIso.supIrredLowerSet.congr_simp : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : Finite α], OrderIso.supIrredLowerSet = OrderIso.supIrredLowerSet
-- Mathlib.RingTheory.Perfection
Perfection.extMonoid : ∀ {M : Type u_1} [inst : CommMonoid M] {p : ℕ} {f g : Perfection M p},
  (∀ (n : ℕ), (Perfection.coeffMonoidHom M p n) f = (Perfection.coeffMonoidHom M p n) g) → f = g
-- Batteries.Data.Vector.Lemmas
Vector.getElem_scanr : ∀ {α : Type u_1} {β : Type u_2} {n i : ℕ} {init : β} {f : α → β → β} {as : Vector α n} (h : i < n + 1),
  (Vector.scanr f init as)[i] = Vector.foldr f init (as.drop i)