mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.VectorField
VectorField.lieBracketWithin_eventually_congr_set : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W : E → E} {s t : Set E} {x : E},
  s =ᶠ[nhds x] t → VectorField.lieBracketWithin 𝕜 V W s =ᶠ[nhds x] VectorField.lieBracketWithin 𝕜 V W t
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
instNontrivialUnitsOfDenselyOrdered : ∀ {α : Type u_1} [inst : LinearOrderedCommGroupWithZero α] [DenselyOrdered α], Nontrivial αˣ
-- Std.Time.DateTime.WallTime
Std.Time.instInhabitedWallTime : Inhabited Std.Time.WallTime
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.superpose_certC.eq_1 : ∀ (k₁ : ℤ) (m₁ : Lean.Grind.CommRing.Mon) (p₁ : Lean.Grind.CommRing.Poly) (k₂ : ℤ) (m₂ : Lean.Grind.CommRing.Mon)
  (p₂ p : Lean.Grind.CommRing.Poly) (c : ℕ),
  Lean.Grind.CommRing.Stepwise.superpose_certC k₁ m₁ p₁ k₂ m₂ p₂ p c =
    ((Lean.Grind.CommRing.Poly.mulMonC k₁ m₁ p₁ c).combineC (Lean.Grind.CommRing.Poly.mulMonC k₂ m₂ p₂ c) c).beq' p
-- Std.Time.Date.Unit.Week
/-- Creates an `Ordinal` from a natural number, ensuring the value is within bounds.
 -/
Std.Time.Week.OfYear.Ordinal.ofNat : (data : ℕ) → autoParam (data ≥ 1 ∧ data ≤ 53) Std.Time.Week.OfYear.Ordinal.ofNat._auto_1 → Std.Time.Week.OfYear.Ordinal
-- Std.Time.Time.Unit.Nanosecond
/-- Creates an `Ordinal` from a natural number, ensuring the value is within bounds.
 -/
Std.Time.Nanosecond.Ordinal.ofNat : (data : ℕ) → data ≤ 999999999 → Std.Time.Nanosecond.Ordinal
-- Mathlib.Computability.Primrec.Basic
Primrec.nat_mod : Primrec₂ fun x1 x2 => x1 % x2
-- Mathlib.GroupTheory.OrderOfElement
/-- The image of an element of finite additive order has finite additive order.  -/
AddMonoidHom.isOfFinAddOrder : ∀ {G : Type u_1} {H : Type u_2} [inst : AddMonoid G] [inst_1 : AddMonoid H] (f : G →+ H) {x : G},
  IsOfFinAddOrder x → IsOfFinAddOrder (f x)
-- Mathlib.Algebra.Field.Subfield.Basic
Field.FG.finitely_generated : ∀ {L : Type v} {inst : DivisionRing L} [self : Field.FG L], ∃ S, Subfield.closure ↑S = ⊤
-- Mathlib.LinearAlgebra.Projectivization.Basic
/-- We define notations `ℙ K V` for the projectivization of the `K`-vector space `V`.  -/
LinearAlgebra.Projectivization.termℙ : Lean.ParserDescr
-- Std.Data.Internal.List.Associative
Std.Internal.List.isEmpty_eq_false_iff_exists_isSome_getValue? : ∀ {α : Type u} {β : Type v} [inst : BEq α] [ReflBEq α] {l : List ((_ : α) × β)},
  l.isEmpty = false ↔ ∃ a, (Std.Internal.List.getValue? a l).isSome = true
-- Mathlib.SetTheory.Ordinal.Notation
ONote.nat : (n : ℕ) → OfNat ONote n
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.abs_sum_of_nonneg : ∀ {ι : Type u_1} {G : Type u_9} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [AddLeftMono G] {f : ι → G}
  {s : Finset ι}, (∀ i ∈ s, 0 ≤ f i) → |∑ i ∈ s, f i| = ∑ i ∈ s, f i
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.iSup_mk : ∀ {α : Type u_2} [inst : TopologicalSpace α] {ι : Sort u_5} (s : ι → Set α) (h : ∀ (i : ι), IsOpen (s i)),
  ⨆ i, { carrier := s i, is_open' := ⋯ } = { carrier := ⋃ i, s i, is_open' := ⋯ }
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.I.homeomorph_zero : TopCat.I.homeomorph 0 = 0
-- Mathlib.CategoryTheory.Monad.Products
/-- The forward direction of the equivalence from coalgebras for the product comonad to the over
category.
 -/
CategoryTheory.coalgebraToOver : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : C) →
      [inst_1 : CategoryTheory.Limits.HasBinaryProducts C] →
        CategoryTheory.Functor (CategoryTheory.prodComonad X).Coalgebra (CategoryTheory.Over X)
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.AECover.iSup_lintegral_eq_of_countably_generated : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι} [Nonempty ι]
  [l.NeBot] [l.IsCountablyGenerated] {φ : ι → Set α},
  MeasureTheory.AECover μ l φ →
    ∀ {f : α → ENNReal}, AEMeasurable f μ → ⨆ i, ∫⁻ (x : α) in φ i, f x ∂μ = ∫⁻ (x : α), f x ∂μ
-- Mathlib.SetTheory.Cardinal.Finite
ENat.card_image_of_injective : ∀ {α : Type u_3} {β : Type u_4} (f : α → β) (s : Set α), Function.Injective f → ENat.card ↑(f '' s) = ENat.card ↑s
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.interSmallerFn.match_1.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    (motive : Option ((a : α) × β a) → Sort u_3) →
      (x : Option ((a : α) × β a)) → ((kv' : (a : α) × β a) → motive (some kv')) → (Unit → motive none) → motive x
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
/-- **Alias** of `Cardinal.lt_power_cof_ord`. -/
Cardinal.lt_power_cof : ∀ {c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → c < c ^ c.ord.cof
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.IterM.forIn_filterMap : ∀ {α : Type u₁} {n : Type u₁ → Type u_1} {β₂ γ : Type u₁} {m : Type u₁ → Type u_2} {β : Type u₁} {ps : Std.Do.PostShape}
  [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n] [LawfulMonad n] [inst_4 : Std.Do.WPMonad n ps]
  [inst_5 : MonadLiftT m n] [LawfulMonadLiftT m n] [inst_7 : Std.Iterator α m β] [Std.Iterators.Finite α m]
  [inst_9 : Std.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n] {it : Std.IterM m β} {f : β → Option β₂} {init : γ}
  {g : β₂ → γ → n (ForInStep γ)} {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond γ ps},
  ⦃P⦄
      forIn it init fun out acc =>
        match f out with
        | some c => g c acc
        | none => pure (ForInStep.yield acc) ⦃Q⦄ →
    ⦃P⦄ forIn (Std.IterM.filterMap f it) init g ⦃Q⦄
-- Mathlib.Order.Hom.Basic
OrderIso.isCompl : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] (f : α ≃o β) {x y : α}, IsCompl x y → IsCompl (f x) (f y)
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.pi_eq_bot_iff : ∀ {η : Type u_7} {f : η → Type u_8} [inst : (i : η) → AddGroup (f i)] (H : (i : η) → AddSubgroup (f i)),
  AddSubgroup.pi Set.univ H = ⊥ ↔ ∀ (i : η), H i = ⊥
-- Mathlib.LinearAlgebra.Lagrange
Polynomial.eq_of_degrees_lt_of_eval_index_eq : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {f g : Polynomial R} {ι : Type u_2} {v : ι → R} (s : Finset ι),
  Set.InjOn v ↑s →
    f.degree < ↑s.card → g.degree < ↑s.card → (∀ i ∈ s, Polynomial.eval (v i) f = Polynomial.eval (v i) g) → f = g
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
fderivWithin_arctan : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E},
  DifferentiableWithinAt ℝ f s x →
    UniqueDiffWithinAt ℝ s x →
      fderivWithin ℝ (fun x => Real.arctan (f x)) s x = (1 / (1 + f x ^ 2)) • fderivWithin ℝ f s x
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
mulLeftReflectLT_of_mulLeftMono : ∀ (N : Type u_2) [inst : Mul N] [inst_1 : LinearOrder N] [MulLeftMono N], MulLeftReflectLT N
-- Mathlib.Topology.Spectral.Hom
SpectralMap.comp_id : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : SpectralMap α β),
  f.comp (SpectralMap.id α) = f
-- Mathlib.Analysis.Meromorphic.Order
/-- On a preconnected set, a meromorphic function has finite order at one point if it has finite
order at another point.  -/
MeromorphicOn.meromorphicOrderAt_ne_top_of_isPreconnected : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} {U : Set 𝕜},
  MeromorphicOn f U →
    ∀ {y : 𝕜}, IsPreconnected U → x ∈ U → y ∈ U → meromorphicOrderAt f x ≠ ⊤ → meromorphicOrderAt f y ≠ ⊤
-- Mathlib.Algebra.EuclideanDomain.Defs
EuclideanDomain.xgcd_zero_left : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] {s t r' s' t' : R},
  EuclideanDomain.xgcdAux 0 s t r' s' t' = (r', s', t')
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.comap_basicOpen : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S) (x : R),
  (TopologicalSpace.Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) (PrimeSpectrum.basicOpen x) =
    PrimeSpectrum.basicOpen (f x)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.dirac_zero : ∀ {β : Type u_2} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] [inst_2 : MeasurableSpace β]
  {x : β}, MeasureTheory.VectorMeasure.dirac x 0 = 0
-- Mathlib.CategoryTheory.FintypeCat
/-- Help typeclass inference infer fullness of forgetful functor.  -/
FintypeCat.instFullForgetFunObjFinite : (CategoryTheory.forget FintypeCat).Full
-- Mathlib.Algebra.Module.LocalizedModule.Int
/-- Given `x : M'`, `M'` a localization of `M` via `f`, `IsInteger f x` iff `x` is in the image of
the localization map `f`.  -/
IsLocalizedModule.IsInteger : {R : Type u_1} →
  [inst : CommSemiring R] →
    {M : Type u_2} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {M' : Type u_3} → [inst_3 : AddCommMonoid M'] → [inst_4 : Module R M'] → (M →ₗ[R] M') → M' → Prop
-- Init.Data.Vector.Extract
Vector.push_extract_getElem : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i j : ℕ} (h : j < n),
  (xs.extract i j).push xs[j] = Vector.cast ⋯ (xs.extract (min i j) (j + 1))
-- Init.Data.Array.Basic
/-- Separates an array of pairs into two arrays that contain the respective first and second components.

Examples:
* `#[("Monday", 1), ("Tuesday", 2)].unzip = (#["Monday", "Tuesday"], #[1, 2])`
* `#[(x₁, y₁), (x₂, y₂), (x₃, y₃)].unzip = (#[x₁, x₂, x₃], #[y₁, y₂, y₃])`
* `(#[] : Array (Nat × String)).unzip = ((#[], #[]) : List Nat × List String)`
 -/
Array.unzip : {α : Type u} → {β : Type u_1} → Array (α × β) → Array α × Array β
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.below.containsThenInsertIfNew₀ : ∀ {α : Type u}
  {motive : {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → (a : Std.DHashMap.Raw α β) → a.WF → Prop}
  {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {h : 0 < m.buckets.size} {a : α}
  {b : β a} (a_1 : m.WF), Std.DHashMap.Raw.WF.below a_1 → motive m a_1 → Std.DHashMap.Raw.WF.below ⋯
-- Mathlib.Order.Filter.Map
Filter.comap_fst_neBot : ∀ {α : Type u_1} {β : Type u_2} [Nonempty β] {f : Filter α} [f.NeBot], (Filter.comap Prod.fst f).NeBot
-- Mathlib.CategoryTheory.Monoidal.Center
/-- Auxiliary construction for `ofBraided`.  -/
CategoryTheory.Center.ofBraidedObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → [CategoryTheory.BraidedCategory C] → C → CategoryTheory.Center C
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.forIn_filterMapWithPostcondition.match_1.splitter : {β₂ : Type u_1} →
  (motive : Option β₂ → Sort u_2) →
    (__do_lift : Option β₂) → ((c : β₂) → motive (some c)) → (Unit → motive none) → motive __do_lift
-- Mathlib.Data.Fin.Tuple.Basic
/-- The beginning of an `n+1` tuple, i.e., its first `n` entries  -/
Fin.init : {n : ℕ} → {α : Fin (n + 1) → Sort u_1} → ((i : Fin (n + 1)) → α i) → (i : Fin n) → α i.castSucc
-- Mathlib.Order.Heyting.Basic
hnot_anti : ∀ {α : Type u_2} [inst : CoheytingAlgebra α], Antitone hnot
-- Init.Data.Bool
Bool.true_beq : ∀ (b : Bool), (true == b) = b
-- Batteries.Recycling.RBTree.Basic
/-- Converts the tree into an array in increasing sorted order.  -/
RBTree.RBNode.toArray : {α : Type u_1} → RBTree.RBNode α → Array α
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
/-- Leading coefficient of powers (in a reduced ring)  -/
MonomialOrder.leadingCoeff_pow : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] [IsReduced R] (f : MvPolynomial σ R)
  (n : ℕ), m.leadingCoeff (f ^ n) = m.leadingCoeff f ^ n
-- Init.Data.UInt.Lemmas
Fin.mk_uInt16ToNat : ∀ (n : UInt16), ⟨n.toNat, ⋯⟩ = n.toFin
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- The map of a Gaussian distribution by multiplication by a constant is a Gaussian.  -/
ProbabilityTheory.gaussianReal_map_mul_const : ∀ {μ : ℝ} {v : NNReal} (c : ℝ),
  MeasureTheory.Measure.map (fun x => x * c) (ProbabilityTheory.gaussianReal μ v) =
    ProbabilityTheory.gaussianReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v)
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.intCast_coeff_zero : ∀ {i : ℤ} {R : Type u_1} [inst : Ring R], (↑i).coeff 0 = ↑i
-- Mathlib.Topology.Algebra.StarSubalgebra
StarSubalgebra.isClosed_topologicalClosure : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : TopologicalSpace A]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : StarRing A] [inst_6 : StarModule R A]
  [inst_7 : IsSemitopologicalSemiring A] [inst_8 : ContinuousStar A] (s : StarSubalgebra R A),
  IsClosed ↑s.topologicalClosure
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- carrier of the algebra  -/
CategoryTheory.Endofunctor.Algebra.a : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C C} → CategoryTheory.Endofunctor.Algebra F → C
-- Lean.Parser.Term
Lean.Parser.Term.let_fun.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.range_add : ∀ {α : Type u_2} [inst : Add α] {ι : Sort u_7} (a : α) (f : ι → α), (Set.range fun i => a + f i) = a +ᵥ Set.range f
-- Mathlib.Topology.Algebra.Module.Compact
Ideal.isCompact_of_fg : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : TopologicalSpace R] [IsTopologicalSemiring R] [CompactSpace R]
  {I : Ideal R}, I.FG → IsCompact ↑I
-- Mathlib.Topology.IsClosedRestrict
Homeomorph.preimageImageRestrict.eq_1 : ∀ {ι : Type u_1} (α : ι → Type u_3) [inst : (i : ι) → TopologicalSpace (α i)] (S : Set ι) (s : Set ((j : ι) → α j)),
  Homeomorph.preimageImageRestrict α S s =
    { toFun := fun x => (⟨Sᶜ.domRestrict ↑x, ⋯⟩, fun i => ↑x ↑i),
      invFun := fun p => ⟨Topology.reorderRestrictProd S s p, ⋯⟩, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯,
      continuous_invFun := ⋯ }
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
PresheafOfModules.freeYonedaCoproductMk.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (M : PresheafOfModules R) (m : M.Elements),
  M.freeYonedaCoproductMk m =
    (CategoryTheory.ConcreteCategory.hom ((M.ιFreeYonedaCoproduct m).app m.fst))
      (ModuleCat.freeMk (CategoryTheory.CategoryStruct.id (Opposite.unop m.fst)))
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- Base change distributes over tensor product.  -/
TensorProduct.AlgebraTensorModule.distribBaseChange : (R : Type uR) →
  (A : Type uA) →
    (N : Type uN) →
      (Q : Type uQ) →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R N] →
                  [inst_5 : AddCommMonoid Q] →
                    [inst_6 : Module R Q] →
                      TensorProduct R A (TensorProduct R N Q) ≃ₗ[A]
                        TensorProduct A (TensorProduct R A N) (TensorProduct R A Q)
-- Mathlib.Order.Interval.Set.SuccPred
Set.Ico_succ_succ_eq_Ioc_of_not_isMax : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {b : α},
  ¬IsMax b → ∀ (a : α), Set.Ico (Order.succ a) (Order.succ b) = Set.Ioc a b
-- Mathlib.LinearAlgebra.InvariantBasisNumber
/-- An `R`-linear map `R^n → R^m` induces a function `R^n/I^n → R^m/I^m`.  -/
_private.Mathlib.LinearAlgebra.InvariantBasisNumber.0.induced_map : {R : Type u} →
  [inst : CommRing R] →
    {ι : Type v} →
      [Fintype ι] →
        {ι' : Type w} →
          (I : Ideal R) → ((ι → R) →ₗ[R] ι' → R) → ((ι → R) ⧸ Ideal.pi fun x => I) → (ι' → R) ⧸ Ideal.pi fun x => I
-- Mathlib.Control.Functor
/-- The map operation for the composition `Comp F G` of functors `F` and `G`.  -/
Functor.Comp.map : {F : Type u → Type w} →
  {G : Type v → Type u} → [Functor F] → [Functor G] → {α β : Type v} → (α → β) → Functor.Comp F G α → Functor.Comp F G β
-- Mathlib.GroupTheory.Congruence.Basic
AddCon.quotientKerEquivOfRightInverse_symm_apply : ∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] (f : M →+ P) (g : P → M)
  (hf : Function.RightInverse g ⇑f) (a : P),
  (AddCon.quotientKerEquivOfRightInverse f g hf).symm a = (AddCon.toQuotient ∘ g) a
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
/-- A `φ`-equivariant morphism induces an equivariant morphism on hom types.  -/
CategoryTheory.IsAddModHom.addActionHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {M : C} →
        [inst_2 : CategoryTheory.AddMonObj M] →
          {X : C} →
            [inst_3 : CategoryTheory.AddModObj M X] →
              {Y : C} →
                [inst_4 : CategoryTheory.AddModObj M Y] →
                  (f : X ⟶ Y) → [CategoryTheory.IsAddModHom M f] → (Z : C) → (Z ⟶ X) →ₑ[id] Z ⟶ Y
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.comp_ι_sq_zero : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {A : Type u_1}
  [inst_3 : Semiring A] [inst_4 : Algebra R A] (g : ExteriorAlgebra R M →ₐ[R] A) (m : M),
  g ((ExteriorAlgebra.ι R) m) * g ((ExteriorAlgebra.ι R) m) = 0
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
MeasureTheory.eLpNorm_condExp_le_eLpNorm : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] (f : α → E) {p : ENNReal},
  1 ≤ p → MeasureTheory.eLpNorm μ[f | m] p μ ≤ MeasureTheory.eLpNorm f p μ
-- Mathlib.Analysis.InnerProductSpace.ExteriorPower
_private.Mathlib.Analysis.InnerProductSpace.ExteriorPower.0.exteriorPower.innerProductForm_eq_sum : ∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {ι : Type u_2}
  [inst_2 : Fintype ι] [inst_3 : LinearOrder ι] (b : OrthonormalBasis ι ℝ E) (x y : ↥(⋀[ℝ]^n E)),
  (exteriorPower.innerProductForm✝ x) y =
    ∑ s, ((Module.Basis.exteriorPower n b.toBasis).repr y) s * ((Module.Basis.exteriorPower n b.toBasis).repr x) s
-- Mathlib.Topology.Semicontinuity.Defs
lowerHemicontinuousWithinAt_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {s : Set α}
  {x : α},
  LowerHemicontinuousWithinAt f s x ↔
    ∀ (u : Set β), IsOpen u → (f x ∩ u).Nonempty → ∀ᶠ (x' : α) in nhdsWithin x s, (f x' ∩ u).Nonempty
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.topologicalSpace_eq_iSup : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} (𝓕 : Filter ι) [inst : (i : ι) → TopologicalSpace (R i)],
  RestrictedProduct.topologicalSpace R A 𝓕 =
    ⨆ S,
      ⨆ (hS : 𝓕 ≤ Filter.principal S),
        TopologicalSpace.coinduced (RestrictedProduct.inclusion R A hS)
          (RestrictedProduct.topologicalSpace R A (Filter.principal S))
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- The quotient map to
the additive quotient of `α` by `G` is measure-preserving between the restriction of `volume` to
an additive fundamental domain in `α` and a related measure satisfying
`AddQuotientMeasureEqMeasurePreimage`.  -/
MeasureTheory.IsAddFundamentalDomain.measurePreserving_add_quotient_mk : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
  {ν : MeasureTheory.Measure α} {𝓕 : Set α},
  MeasureTheory.IsAddFundamentalDomain G 𝓕 ν →
    ∀ (μ : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α)))
      [MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ],
      MeasureTheory.MeasurePreserving (Quotient.mk (AddAction.orbitRel G α)) (ν.restrict 𝓕) μ
-- Std.Data.HashSet.Lemmas
Std.HashSet.get!_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] [inst : Inhabited α]
  {f : α → Bool} {k : α}, (Std.HashSet.filter f m).get! k = (Option.filter f (m.get? k)).get!
-- Mathlib.ModelTheory.LanguageMap
/-- Gives a `constantsOn α` structure to a type by assigning each constant a value.  -/
FirstOrder.Language.constantsOn.structure : {M : Type w} → {α : Type u'} → (α → M) → (FirstOrder.Language.constantsOn α).Structure M
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Cont'.comp : Turing.ToPartrec.Code → Turing.PartrecToTM2.Cont' → Turing.PartrecToTM2.Cont'
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.hasFiniteIntegral_toReal_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  (∀ᵐ (x : α) ∂μ, f x ≠ ⊤) → (MeasureTheory.HasFiniteIntegral (fun x => (f x).toReal) μ ↔ ∫⁻ (x : α), f x ∂μ ≠ ⊤)
-- Lean.Elab.Tactic.Doc
/-- The information needed to display all documentation for a tactic.
 -/
Lean.Elab.Tactic.Doc.TacticDoc : Type
-- Mathlib.SetTheory.Lists
Lists.Subset.decidable.eq_def : ∀ {α : Type u_1} [inst : DecidableEq α] (x x_1 : Lists' α true),
  Lists.Subset.decidable x x_1 =
    match x, x_1 with
    | Lists'.nil, x => isTrue ⋯
    | a.cons' l₁, l₂ => decidable_of_iff' (⟨b, a⟩ ∈ l₂ ∧ l₁ ⊆ l₂) ⋯
-- Lean.Elab.PreDefinition.WF.Unfold
/-- Derives the equational theorem for the individual functions from the equational
theorem of `foo._unary` or `foo._binary`.

It should just be a specialization of that one, due to defeq.
 -/
Lean.Elab.WF.mkBinaryUnfoldEq : Lean.Elab.PreDefinition → Lean.Name → Lean.MetaM Unit
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.decidableMemPowers.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] {a : M},
  Submonoid.decidableMemPowers = Classical.decPred fun x => x ∈ Submonoid.powers a
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.addOppositeEquiv_symm_support : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddMonoid R] (x : (HahnSeries Γ R)ᵃᵒᵖ),
  (HahnSeries.addOppositeEquiv.symm x).support = (AddOpposite.unop x).support
-- Mathlib.Algebra.Lie.Sl2
IsSl2Triple.HasPrimitiveVectorWith.lie_e : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {h e f : L} {t : IsSl2Triple h e f} {m : M} {μ : R},
  t.HasPrimitiveVectorWith m μ → ⁅e, m⁆ = 0
-- Mathlib.Order.Interval.Finset.Fin
Fin.instLocallyFiniteOrderTop : (n : ℕ) → LocallyFiniteOrderTop (Fin n)
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.measurePreserving_eval : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] (i : ι),
  MeasureTheory.MeasurePreserving (Function.eval i) (MeasureTheory.Measure.pi μ) (μ i)
-- Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
isClosedMap_dist : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [ProperSpace α] (x : α), IsClosedMap (dist x)
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.SimprocsArray.add : Lean.Meta.Simp.SimprocsArray → Lean.Name → Bool → Lean.CoreM Lean.Meta.Simp.SimprocsArray
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.sigmaObj.congr_simp : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f f_1 : β → C) (e_f : f = f_1)
  [inst_1 : CategoryTheory.Limits.HasCoproduct f], ∐ f = ∐ f_1
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.degreeLT_mono : ∀ {R : Type u} [inst : Semiring R] {m n : ℕ}, m ≤ n → Polynomial.degreeLT R m ≤ Polynomial.degreeLT R n
-- Mathlib.Analysis.Normed.Group.Quotient
QuotientAddGroup.quotientBotIsometryEquiv.eq_1 : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M],
  QuotientAddGroup.quotientBotIsometryEquiv = { toEquiv := QuotientAddGroup.quotientBot.toEquiv, isometry_toFun := ⋯ }
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.disjoint_openCell_of_ne`. -/
Topology.CWComplex.disjoint_openCell_of_ne : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] {n m : ℕ}
  {i : Topology.RelCWComplex.cell C n} {j : Topology.RelCWComplex.cell C m},
  ⟨n, i⟩ ≠ ⟨m, j⟩ → Disjoint (Topology.RelCWComplex.openCell n i) (Topology.RelCWComplex.openCell m j)
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.lift_lt_omega_one : ∀ {o : Ordinal.{u}}, Ordinal.lift.{v, u} o < Ordinal.omega 1 ↔ o < Ordinal.omega 1