mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.MeasurableSpace.Pi
/-- If `C` and `D` generate the σ-algebras on `α` resp. `β`, then rectangles formed by `C` and `D`
generate the σ-algebra on `α × β`.  -/
generateFrom_eq_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} [Finite ι] [h : (i : ι) → MeasurableSpace (α i)] {C : (i : ι) → Set (Set (α i))},
  (∀ (i : ι), MeasurableSpace.generateFrom (C i) = h i) →
    (∀ (i : ι), IsCountablySpanning (C i)) →
      MeasurableSpace.generateFrom (Set.univ.pi '' Set.univ.pi C) = MeasurableSpace.pi
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.isEmpty_eq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₁.Equiv m₂ → m₁.isEmpty = m₂.isEmpty
-- Batteries.Control.LawfulMonadState
liftM_modify : ∀ {σ : Type u_1} {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [inst : MonadStateOf σ m] [inst_1 : MonadLift m n]
  (f : σ → σ), liftM (modify f) = modify f
-- Mathlib.GroupTheory.GroupAction.Quotient
/-- **Burnside's lemma** : given a finite additive group `G` acting on a type `X`,
the sum the orders of the stabilisers coincides with the number of orbits multiplied by the
order of `G`. 

[Wikidata Q1330377](https://www.wikidata.org/wiki/Q1330377) -/
AddAction.sum_card_fixedBy_eq_card_orbits_mul_card_addGroup : ∀ (G : Type u) (X : Type v) [inst : AddGroup G] [inst_1 : AddAction G X] [inst_2 : Fintype G]
  [inst_3 : (g : G) → Fintype ↑(AddAction.fixedBy X g)] [inst_4 : Fintype (Quotient (AddAction.orbitRel G X))],
  ∑ g, Fintype.card ↑(AddAction.fixedBy X g) = Fintype.card (Quotient (AddAction.orbitRel G X)) * Fintype.card G
-- Mathlib.Logic.Encodable.Basic
Encodable.decode_sigma_val : ∀ {α : Type u_1} {γ : α → Type u_3} [inst : Encodable α] [inst_1 : (a : α) → Encodable (γ a)] (n : ℕ),
  Encodable.decode n =
    (Encodable.decode (Nat.unpair n).1).bind fun a => Option.map (Sigma.mk a) (Encodable.decode (Nat.unpair n).2)
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.MonoOver.inf_map_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {A : C}
  {X Y : CategoryTheory.MonoOver A} (k : X ⟶ Y) (g : CategoryTheory.MonoOver A),
  (CategoryTheory.MonoOver.inf.map k).app g =
    CategoryTheory.MonoOver.homMk
      (CategoryTheory.Limits.pullback.lift
        (CategoryTheory.Limits.pullback.fst ((CategoryTheory.MonoOver.forget A).obj g).hom X.arrow)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.snd ((CategoryTheory.MonoOver.forget A).obj g).hom X.arrow)
          (CategoryTheory.Over.Hom.left k.hom))
        ⋯)
      ⋯
-- Mathlib.RingTheory.LocalRing.Quotient
/-- Given a basis of `S`, the induced basis of `S / Ideal.map (algebraMap R S) p`.  -/
IsLocalRing.basisQuotient : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          [inst_3 : IsLocalRing R] →
            [Module.Finite R S] →
              [Module.Free R S] →
                {ι : Type u_3} →
                  [Fintype ι] →
                    Module.Basis ι R S →
                      Module.Basis ι (R ⧸ IsLocalRing.maximalIdeal R)
                        (S ⧸ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R))
-- Mathlib.Algebra.Order.Ring.Pow
/-- **Bernoulli's inequality** for `n : ℕ`, `-2 ≤ a`.  -/
one_add_mul_le_pow : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a : R},
  -2 ≤ a → ∀ (n : ℕ), 1 + ↑n * a ≤ (1 + a) ^ n
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Hom.zero_def : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M X : C} [inst_2 : CategoryTheory.AddMonObj M],
  0 =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X)
      CategoryTheory.AddMonObj.zero
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Term.restrictVar.eq_def : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} [inst : DecidableEq α] (x : L.Term α) (x_1 : ↥x.varFinset → β),
  x.restrictVar x_1 =
    match x, x_1 with
    | FirstOrder.Language.var a, f => FirstOrder.Language.var (f ⟨a, ⋯⟩)
    | FirstOrder.Language.func F ts, f => FirstOrder.Language.func F fun i => (ts i).restrictVar (f ∘ Set.inclusion ⋯)
-- Mathlib.MeasureTheory.Measure.Restrict
indicator_meas_zero : ∀ {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f : α → β}
  [inst_1 : Zero β], μ s = 0 → s.indicator f =ᵐ[μ] 0
-- Mathlib.NumberTheory.RatFunc.Ostrowski
RatFunc.irreducible_min_polynomial_valuation_lt_one_and_ne_zero : ∀ {K : Type u_1} {Γ : Type u_2} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ]
  {v : Valuation (RatFunc K) Γ} [Valuation.IsTrivialOn K v] (hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty),
  Irreducible (⋯.min {p | v ↑p < 1 ∧ p ≠ 0} hne)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
HasDerivWithinAt.csin : ∀ {f : ℂ → ℂ} {f' x : ℂ} {s : Set ℂ},
  HasDerivWithinAt f f' s x → HasDerivWithinAt (fun x => Complex.sin (f x)) (Complex.cos (f x) * f') s x
-- Mathlib.Tactic.Linter.DocString
/-- The "empty doc string" warns on empty doc-strings.
 -/
Mathlib.Linter.linter.style.docString.empty : Lean.Option Bool
-- Mathlib.Order.SuccPred.Archimedean
StrictMono.not_bddAbove_range_of_isSuccArchimedean : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [Nonempty α] [inst_2 : Preorder β] {f : α → β} [NoMaxOrder α]
  [inst_4 : SuccOrder β] [IsSuccArchimedean β], StrictMono f → ¬BddAbove (Set.range f)
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.reflection_indexEquiv : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i : ι),
  (↑(RootPairing.Equiv.reflection P i)).indexEquiv = P.reflectionPerm i
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightIso_unitIso_inv_app_left : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) (X : CategoryTheory.Comma L R₁),
  ((CategoryTheory.Comma.mapRightIso L i).unitIso.inv.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Order.Comparable
LE.le.not_incompRel : ∀ {α : Type u_1} {a b : α} [inst : LE α], a ≤ b → ¬IncompRel (fun x1 x2 => x1 ≤ x2) a b
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.maxKey?_modify : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {f : β → β},
  (Std.DTreeMap.Const.modify t k f).maxKey? = Option.map (fun km => if cmp km k = Ordering.eq then k else km) t.maxKey?
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.isEquivalent_sinh : Asymptotics.IsEquivalent (nhds 0) Real.sinh id
-- Mathlib.Topology.Semicontinuity.Defs
LowerSemicontinuousOn.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace γ]
  [inst_2 : Preorder β] {f : α → β} {s : Set α} {g : γ → α} {t : Set γ},
  LowerSemicontinuousOn f s → ContinuousOn g t → Set.MapsTo g t s → LowerSemicontinuousOn (f ∘ g) t
-- Lean.Data.PersistentArray
Lean.PersistentArray.findSomeM? : {α : Type u} →
  {m : Type v → Type w} → [Monad m] → {β : Type v} → Lean.PersistentArray α → (α → m (Option β)) → m (Option β)
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.mem_center_iff_spec : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : Module.Free R V] [inst_4 : Module.Finite R V] {g : SpecialLinearGroup R V}
  (hg : g ∈ Subgroup.center (SpecialLinearGroup R V)) (x : V), ↑↑g x = ⋯.choose • x
-- Mathlib.Analysis.Normed.Algebra.Unitization
/-- This is often the more useful lemma to rewrite the norm as opposed to
`Unitization.nnnorm_def`.  -/
Unitization.nnnorm_eq_sup : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : IsScalarTower 𝕜 A A] [inst_4 : SMulCommClass 𝕜 A A]
  [inst_5 : RegularNormedAlgebra 𝕜 A] (x : Unitization 𝕜 A),
  ‖x‖₊ = max ‖x.toProd.1‖₊ ‖(algebraMap 𝕜 (A →L[𝕜] A)) x.toProd.1 + (ContinuousLinearMap.mul 𝕜 A) x.toProd.2‖₊
-- Mathlib.Algebra.Module.CharacterModule
CharacterModule.dual_surjective_of_injective : ∀ {R : Type uR} [inst : CommRing R] {A : Type uA} [inst_1 : AddCommGroup A] {B : Type uB} [inst_2 : AddCommGroup B]
  [inst_3 : Module R A] [inst_4 : Module R B] (f : A →ₗ[R] B),
  Function.Injective ⇑f → Function.Surjective ⇑(CharacterModule.dual f)
-- Std.Tactic.BVDecide.LRAT.Parser
Std.Tactic.BVDecide.LRAT.Parser.Binary.parseId : Std.Internal.Parsec.ByteArray.Parser ℕ
-- Std.Internal.Do.Order.Basic
Lean.Order.le_iSup : ∀ {α : Type u} [inst : Lean.Order.CompleteLattice α] {ι : Type v} (f : ι → α) (i : ι),
  Lean.Order.PartialOrder.rel (f i) (Lean.Order.iSup f)
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.instMonoOfLEMk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A : C} (X : CategoryTheory.Subobject B) (f : A ⟶ B)
  [inst_1 : CategoryTheory.Mono f] (h : X ≤ CategoryTheory.Subobject.mk f), CategoryTheory.Mono (X.ofLEMk f h)
-- Mathlib.Data.ENNReal.Operations
ENNReal.add_sub_cancel_left : ∀ {a b : ENNReal}, a ≠ ⊤ → a + b - a = b
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.eq_empty_of_insertManyIfNewUnit_eq_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtDHashMap α fun x => Unit} {ρ : Type w} [inst : ForIn Id ρ α]
  [inst_1 : EquivBEq α] [inst_2 : LawfulHashable α] {l : ρ}, Std.ExtDHashMap.Const.insertManyIfNewUnit m l = ∅ → m = ∅
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.isLongestMatch_iff_isLongestMatch_toSlice : ∀ {pat : String} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatch pat pos ↔ String.Slice.Pattern.Model.IsLongestMatch pat.toSlice pos
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_eq_some_get! : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  [inst_4 : Inhabited α], m.WF → ∀ {a : α}, a ∈ m → m.get? a = some (m.get! a)
-- Mathlib.Algebra.Category.AlgCat.TensorAlgebra
AlgCat.tensorAlgebraAdj_counit_app : ∀ (R : Type u) [inst : CommRing R] (A : AlgCat R),
  (AlgCat.tensorAlgebraAdj R).counit.app A = AlgCat.ofHom ((TensorAlgebra.lift R) LinearMap.id)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.coeFn_mk : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f : α →ₘ[μ] E} (hf : MeasureTheory.eLpNorm (↑f) p μ < ⊤), ↑↑⟨f, hf⟩ = ↑f
-- Mathlib.MeasureTheory.SetAlgebra
MeasureTheory.IsSetAlgebra.empty_mem : ∀ {α : Type u_1} {𝒜 : Set (Set α)}, MeasureTheory.IsSetAlgebra 𝒜 → ∅ ∈ 𝒜
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.coe_star : ∀ (z : Complex.UnitDisc), ↑(star z) = (starRingEnd ℂ) ↑z
-- Mathlib.RingTheory.MatrixAlgebra
/-- The function `(A ⊗[R] Matrix n n R) →ₐ[R] Matrix n n A`, as an algebra homomorphism.
 -/
MatrixEquivTensor.toFunAlgHom : (n : Type u_3) →
  (R : Type u_5) →
    (A : Type u_7) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : DecidableEq n] → [inst_4 : Fintype n] → TensorProduct R A (Matrix n n R) →ₐ[R] Matrix n n A
-- Mathlib.RingTheory.Ideal.Basic
Ring.not_isField_iff_exists_prime : ∀ {R : Type u_5} [inst : CommSemiring R] [Nontrivial R], ¬IsField R ↔ ∃ p, p ≠ ⊥ ∧ p.IsPrime
-- Mathlib.Data.Set.Pairwise.Lattice
Set.pairwiseDisjoint_pair_insert : ∀ {α : Type u_1} {s : Set α} {a : α}, a ∉ s → (𝒫 s).PairwiseDisjoint fun t => {t, insert a t}
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec32_not : ∀ {a : ISize} (h : System.Platform.numBits = 32), (~~~a).toBitVec32 h = ~~~a.toBitVec32 h
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.coe_toContinuousLinearMap : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂), ⇑f.toContinuousLinearMap = ⇑f
-- Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
SSet.instHasDimensionLETensorObjHAddNat : ∀ {X₁ X₂ : SSet} (d₁ d₂ : ℕ) [X₁.HasDimensionLE d₁] [X₂.HasDimensionLE d₂],
  (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂).HasDimensionLE (d₁ + d₂)
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Tries to find a ground pattern to activate the theorem.
This is used for theorems such as `theorem evenZ : Even 0`.
This function is only used if `collectPatterns?` returns `none`.

Remark: only symbols with priority `>= minPrio` are considered.
 -/
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.collectGroundPattern? : Lean.Expr →
  Array Lean.Expr →
    Array Lean.Expr → Lean.Meta.Grind.SymbolPriorities → ℕ → Lean.MetaM (Option (Lean.Expr × List Lean.HeadIndex))
-- Mathlib.Data.Rel
SetRel.mem_preimage : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α β} {t : Set β} {a : α}, a ∈ R.preimage t ↔ ∃ b ∈ t, (a, b) ∈ R
-- Mathlib.Topology.Algebra.GroupWithZero
Continuous.div_const : ∀ {α : Type u_1} {G₀ : Type u_3} [inst : DivInvMonoid G₀] [inst_1 : TopologicalSpace G₀] [SeparatelyContinuousMul G₀]
  {f : α → G₀} [inst_3 : TopologicalSpace α], Continuous f → ∀ (y : G₀), Continuous fun x => f x / y
-- Init.Grind.Lemmas
Lean.Grind.Bool.eq_true_of_not_eq_false : ∀ {a : Bool}, (!a) = false → a = true
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
algebraicIndependent_empty : ∀ {A : Type v} [inst : CommRing A] {K : Type u_3} [inst_1 : Field K] [inst_2 : Algebra K A] [Nontrivial A],
  AlgebraicIndependent K Subtype.val
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
/-- The precylinder in a full subcategory of `C` induced by a precylinder
in the category `C`.  -/
HomotopicalAlgebra.Precylinder.toFullSubcategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {P : CategoryTheory.ObjectProperty C} →
      {X : P.FullSubcategory} → (Q : HomotopicalAlgebra.Precylinder X.obj) → P Q.I → HomotopicalAlgebra.Precylinder X
-- Mathlib.Topology.VectorBundle.Riemannian
Bundle.ContinuousRiemannianMetric.isVonNBounded : ∀ {B : Type u_4} [inst : TopologicalSpace B] {F : Type u_5} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  {E : B → Type u_6} [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : (b : B) → TopologicalSpace (E b)]
  [inst_5 : (b : B) → AddCommGroup (E b)] [inst_6 : (b : B) → Module ℝ (E b)] [inst_7 : FiberBundle F E]
  [inst_8 : VectorBundle ℝ F E] (self : Bundle.ContinuousRiemannianMetric F E) (b : B),
  Bornology.IsVonNBounded ℝ {v | ((self.inner b) v) v < 1}
-- Mathlib.Algebra.Homology.Embedding.HomEquiv
/-- Given `φ : K.restriction e ⟶ L` such that `hφ : e.HasLift φ`, this is
the isomorphisms in the category of arrows between the maps
`(e.liftExtend φ hφ).f i'` and `φ.f i` when `e.f i = i'`.  -/
ComplexShape.Embedding.liftExtendfArrowIso : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        (e : c.Embedding c') →
          {C : Type u_3} →
            [inst : CategoryTheory.Category.{v_1, u_3} C] →
              [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
                [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
                  {K : HomologicalComplex C c'} →
                    {L : HomologicalComplex C c} →
                      [inst_3 : e.IsRelIff] →
                        (φ : K.restriction e ⟶ L) →
                          (hφ : e.HasLift φ) →
                            {i' : ι'} →
                              {i : ι} →
                                e.f i = i' →
                                  (CategoryTheory.Arrow.mk ((e.liftExtend φ hφ).f i') ≅ CategoryTheory.Arrow.mk (φ.f i))
-- Mathlib.RingTheory.Localization.Basic
/-- Injectivity of the underlying `algebraMap` descends to the algebra induced by localization.  -/
localizationAlgebra_injective : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] (Rₘ : Type u_4) (Sₘ : Type u_5) [inst_3 : CommSemiring Rₘ] [inst_4 : CommSemiring Sₘ]
  [inst_5 : Algebra R Rₘ] [inst_6 : IsLocalization M Rₘ] [inst_7 : Algebra S Sₘ]
  [i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ],
  Function.Injective ⇑(algebraMap R S) → Function.Injective ⇑(algebraMap Rₘ Sₘ)
-- Mathlib.Order.Category.HeytAlg
HeytAlg.Hom.ext_iff : ∀ {X Y : HeytAlg} {x y : X.Hom Y}, x = y ↔ x.hom' = y.hom'
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.two_div_one_sub_two_div_e_le_eight : 2 / (1 - 2 / Real.exp 1) ≤ 8
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.BuilderOption.immediate : Array Lean.Name → Aesop.Frontend.BuilderOption
-- Mathlib.SetTheory.Lists
Lists.Equiv.antisymm_iff : ∀ {α : Type u_1} {l₁ l₂ : Lists' α true}, (Lists.of' l₁).Equiv (Lists.of' l₂) ↔ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁
-- Mathlib.CategoryTheory.Triangulated.Opposite.Functor
CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_inv_app_unop : ∀ {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.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ] (X : Cᵒᵖ) (n : ℤ),
  F.map ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app X).unop =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence D n).unitIso.inv.app
          (Opposite.op (F.obj (Opposite.unop X)))).unop
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor D n).map ((CategoryTheory.Functor.commShiftIso F.op n).hom.app X).unop)
        ((CategoryTheory.Functor.commShiftIso F n).inv.app (Opposite.unop ((CategoryTheory.shiftFunctor Cᵒᵖ n).obj X))))
-- Mathlib.MeasureTheory.Measure.Haar.OfBasis
/-- Let `μ` be a σ-finite left invariant measure on `E`. Then `μ` is equal to the Haar measure
defined by `b` iff the parallelepiped defined by `b` has measure `1` for `μ`.  -/
Module.Basis.addHaar_eq_iff : ∀ {ι : Type u_1} {E : Type u_3} [inst : Fintype ι] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] [SecondCountableTopology E] (b : Module.Basis ι ℝ E)
  (μ : MeasureTheory.Measure E) [MeasureTheory.SigmaFinite μ] [μ.IsAddLeftInvariant],
  b.addHaar = μ ↔ μ ↑b.parallelepiped = 1
-- Mathlib.Algebra.Order.ToIntervalMod
/-- **Alias** of the forward direction of `AddCommGroup.modEq_iff_toIcoMod_eq_left`. -/
AddCommGroup.ModEq.toIcoMod_eq_left : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) {a b : α}, a ≡ b [PMOD p] → toIcoMod hp a b = a
-- Init.Data.Vector.Lemmas
Vector.foldlM_pure : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {n : ℕ} [inst : Monad m] [LawfulMonad m] {f : β → α → β}
  {b : β} {xs : Vector α n}, Vector.foldlM (fun x1 x2 => pure (f x1 x2)) b xs = pure (Vector.foldl f b xs)
-- Init.Data.Fin.Lemmas
Fin.last_zero : Fin.last 0 = 0
-- Mathlib.Data.Matrix.Mul
/-- `M *ᵥ v` (notation for `mulVec M v`) is the matrix-vector product of matrix `M` and vector `v`,
where `v` is seen as a column vector.

The notation has precedence 73, which comes immediately before ` ⬝ᵥ ` for `dotProduct`,
so that `A *ᵥ v ⬝ᵥ B *ᵥ w` is parsed as `(A *ᵥ v) ⬝ᵥ (B *ᵥ w)`.
 -/
Matrix.«term_*ᵥ_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Quaternion
Quaternion.imK_equivProd_symm_apply : ∀ (R : Type u_1) [inst : Zero R] [inst_1 : One R] [inst_2 : Neg R] (a : R × R × R × R),
  ((Quaternion.equivProd R).symm a).imK = a.2.2.2
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
/-- The preimage of a basic open in `Spec Γ(X)` under the unit is the basic
open in `X` defined by the same element (they are equal as sets).  -/
AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_basicOpen_eq : ∀ (X : AlgebraicGeometry.LocallyRingedSpace) (r : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))),
  X.toΓSpecFun ⁻¹' ↑(PrimeSpectrum.basicOpen r) = ↑(X.toRingedSpace.basicOpen r)
-- Init.Data.UInt.Lemmas
UInt32.toUInt16_mod : ∀ (a b : UInt32), a < 65536 → b < 65536 → (a % b).toUInt16 = a.toUInt16 % b.toUInt16
-- Mathlib.Algebra.Category.ModuleCat.Limits
ModuleCat.directLimitCocone_ι_app : ∀ {R : Type u} [inst : Ring R] {ι : Type v} [inst_1 : DecidableEq ι] [inst_2 : Preorder ι] (G : ι → Type v)
  [inst_3 : (i : ι) → AddCommGroup (G i)] [inst_4 : (i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
  [inst_5 : DirectedSystem G fun i j h => ⇑(f i j h)] (x : ι),
  (ModuleCat.directLimitCocone G f).ι.app x = ModuleCat.ofHom (Module.DirectLimit.of R ι G f x)
-- Mathlib.Data.NNRat.BigOperators
NNRat.cast_listProd : ∀ {K : Type u_2} [inst : DivisionSemiring K] [CharZero K] (l : List ℚ≥0), ↑l.prod = (List.map NNRat.cast l).prod
-- Mathlib.Order.Filter.Prod
Filter.eventually_prod_iff : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} {p : α × β → Prop},
  (∀ᶠ (x : α × β) in f ×ˢ g, p x) ↔
    ∃ pa, (∀ᶠ (x : α) in f, pa x) ∧ ∃ pb, (∀ᶠ (y : β) in g, pb y) ∧ ∀ {x : α}, pa x → ∀ {y : β}, pb y → p (x, y)
-- Mathlib.InformationTheory.Hamming
Hamming.toHamming_symm_eq : ∀ {ι : Type u_2} {β : ι → Type u_3}, Hamming.toHamming.symm = Hamming.ofHamming
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
/-- Given a property of germs of functions and sets in the model space, then one defines
a corresponding property in a charted space, by requiring that it holds at the preferred chart at
this point. (When the property is local and invariant, it will in fact hold using any chart, see
`liftPropWithinAt_indep_chart`). We require continuity in the lifted property, as otherwise one
single chart might fail to capture the behavior of the function.
 -/
ChartedSpace.LiftPropWithinAt : {H : Type u_1} →
  {M : Type u_2} →
    {H' : Type u_3} →
      {M' : Type u_4} →
        [inst : TopologicalSpace H] →
          [inst_1 : TopologicalSpace M] →
            [ChartedSpace H M] →
              [inst : TopologicalSpace H'] →
                [inst_2 : TopologicalSpace M'] →
                  [ChartedSpace H' M'] → ((H → H') → Set H → H → Prop) → (M → M') → Set M → M → Prop
-- Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
Real.tsum_exp_neg_mul_int_sq : ∀ {a : ℝ},
  0 < a → ∑' (n : ℤ), Real.exp (-Real.pi * a * ↑n ^ 2) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), Real.exp (-Real.pi / a * ↑n ^ 2)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
/-- Summability of the divisor-sum q-expansion series `∑ σ_{k-1}(n) q^n`.  -/
EisensteinSeries.summable_sigma_mul_cexp_pow : ∀ {k : ℕ},
  1 ≤ k →
    ∀ (z : UpperHalfPlane),
      Summable fun n => ↑((ArithmeticFunction.sigma (k - 1)) n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ n
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.opNorm_mapLMultilinear_le : ∀ {ι : Type u_1} [inst : Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] {E' : ι → Type u_5}
  [inst_4 : (i : ι) → SeminormedAddCommGroup (E' i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (E' i)],
  ‖PiTensorProduct.mapLMultilinear 𝕜 E E'‖ ≤ 1
-- Mathlib.Data.ENat.Basic
instSuccOrderENat : SuccOrder ℕ∞
-- Init.Grind.AC
Lean.Grind.AC.instBEqSeq.beq : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Bool