mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Notation.Indicator
Set.mulIndicator_one_preimage : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] {t : Set α} (s : Set M), t.mulIndicator 1 ⁻¹' s ∈ {Set.univ, ∅}
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.ne_zero : ∀ (z : UpperHalfPlane), ↑z ≠ 0
-- Mathlib.Order.WithBot
WithBot.noTopOrder : ∀ {α : Type u_1} [inst : LE α] [NoTopOrder α] [Nonempty α], NoTopOrder (WithBot α)
-- Mathlib.Algebra.Free
FreeAddMagma.length_toFreeAddSemigroup : ∀ {α : Type u} (x : FreeAddMagma α), (FreeAddMagma.toFreeAddSemigroup x).length = x.length
-- Mathlib.Algebra.Lie.Semisimple.Basic
LieAlgebra.hasTrivialRadical_iff_no_abelian_ideals : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  LieAlgebra.HasTrivialRadical R L ↔ ∀ (I : LieIdeal R L), IsLieAbelian ↥I → I = ⊥
-- Mathlib.MeasureTheory.Function.AEEqOfIntegral
/-- If a locally integrable function has zero integral on all compact sets in a sigma-compact space,
then it is zero almost everywhere.  -/
MeasureTheory.ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero' : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {β : Type u_3}
  [inst_3 : TopologicalSpace β] [inst_4 : MeasurableSpace β] [BorelSpace β] [SigmaCompactSpace β] [R1Space β]
  {μ : MeasureTheory.Measure β} {f : β → E},
  MeasureTheory.LocallyIntegrable f μ → (∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0) → f =ᵐ[μ] 0
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.instCategoryProEt : (S : AlgebraicGeometry.Scheme) → CategoryTheory.Category.{u_1, u_1 + 1} S.ProEt
-- Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
/-- A measurable set such that `μ.restrict (μ.sigmaFiniteSetGE ν n)` is sigma-finite and
for `C` the supremum of `ν s` over all measurable sets `s` with `μ.restrict s` sigma-finite,
`ν (μ.sigmaFiniteSetGE ν n) ≥ C - 1/n`.  -/
MeasureTheory.Measure.sigmaFiniteSetGE : {α : Type u_1} →
  {mα : MeasurableSpace α} →
    MeasureTheory.Measure α → (ν : MeasureTheory.Measure α) → [MeasureTheory.IsFiniteMeasure ν] → ℕ → Set α
-- Init.Tactics
/-- `mexfalso` is like `exfalso`, but operating on a stateful `Std.Do.SPred` goal.
```lean
example (P : SPred σs) : ⌜False⌝ ⊢ₛ P := by
  mintro HP
  mexfalso
  mexact HP
```
 -/
Lean.Parser.Tactic.mexfalsoMacro : Lean.ParserDescr
-- Init.Data.AC
Lean.Data.AC.Context.evalList_sort : ∀ {α : Sort u_1} (ctx : Lean.Data.AC.Context α),
  Lean.Data.AC.ContextInformation.isComm ctx = true →
    ∀ (e : List ℕ), Lean.Data.AC.evalList α ctx (Lean.Data.AC.sort e) = Lean.Data.AC.evalList α ctx e
-- Lean.Setup
Lean.Plugin.mk.inj : ∀ {path : System.FilePath} {initFn? : Option String} {path_1 : System.FilePath} {initFn?_1 : Option String},
  { path := path, initFn? := initFn? } = { path := path_1, initFn? := initFn?_1 } → path = path_1 ∧ initFn? = initFn?_1
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
tangentMapWithin.eq_1 : ∀ {𝕜 : 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') (s : Set M)
  (p : TangentBundle I M), tangentMapWithin I I' f s p = ⟨f p.proj, (mfderiv[s] f p.proj) p.snd⟩
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.unop_φH : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex Cᵒᵖ} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
  (ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂), ψ.unop.φH = ψ.φH.unop
-- Lean.Meta.Tactic.NormCast
/-- A simp set which simplifies transitive coercions.  -/
Lean.Meta.NormCast.NormCastExtension.squash : Lean.Meta.NormCast.NormCastExtension → Lean.Meta.SimpExtension
-- Init.Data.List.Basic
List.map_cons : ∀ {α : Type u} {β : Type v} {f : α → β} {a : α} {l : List α}, List.map f (a :: l) = f a :: List.map f l
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- See also `Ideal.IsMaximal.mem_pow_mul` for maximal ideal.  -/
Ideal.IsPrime.mem_pow_mul : ∀ {R : Type u_1} [inst : CommRing R] [IsDedekindDomain R] (I : Ideal R) [hI : I.IsPrime] {a b : R} {n : ℕ},
  a * b ∈ I ^ n → a ∈ I ^ n ∨ b ∈ I
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.toNat : Lean.Lsp.SemanticTokenType → ℕ
-- Mathlib.Data.Finsupp.Basic
Finsupp.subtypeDomain_neg : ∀ {α : Type u_1} {G : Type u_8} [inst : AddGroup G] {p : α → Prop} {v : α →₀ G},
  Finsupp.subtypeDomain p (-v) = -Finsupp.subtypeDomain p v
-- Init.Data.Nat.Gcd
Nat.gcd_add_self_right : ∀ (m n : ℕ), m.gcd (n + m) = m.gcd n
-- Init.Data.Float.Float
/-- Computes the square root of a floating-point number.

This function has a logical model in terms of `Float.Model`. It is implemented in compiled code by the
C function `sqrt`.
 -/
Float.sqrt : Float → Float
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
unitInterval.sigmoid_lt_iff : ∀ {a b : ℝ}, unitInterval.sigmoid a < unitInterval.sigmoid b ↔ a < b
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_le_one : ∀ {x : ENNReal} {z : ℝ}, x ≤ 1 → 0 ≤ z → x ^ z ≤ 1
-- Mathlib.Algebra.Homology.Embedding.IsSupported
HomologicalComplex.isSupportedOutside_op_iff : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c'), K.op.IsSupportedOutside e.op ↔ K.IsSupportedOutside e
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkDoneProgressBegin.mk : Lean.Lsp.WorkDoneProgressReport → String → Lean.Lsp.WorkDoneProgressBegin
-- Mathlib.Analysis.Analytic.Composition
FormalMultilinearSeries.removeZero_applyComposition : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  [inst_7 : IsTopologicalAddGroup E] [inst_8 : ContinuousConstSMul 𝕜 E] [inst_9 : IsTopologicalAddGroup F]
  [inst_10 : ContinuousConstSMul 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (c : Composition n),
  p.removeZero.applyComposition c = p.applyComposition c
-- Mathlib.Algebra.NonAssoc.PreLie.Basic
LeftPreLieRing.mk : {L : Type u_1} →
  [toNonUnitalNonAssocRing : NonUnitalNonAssocRing L] →
    (∀ (x y z : L), associator x y z = associator y x z) → LeftPreLieRing L
-- Mathlib.Analysis.Normed.Lp.Matrix
LinearMap.det_toLpLin : ∀ {ι : Type u_5} {R : Type u_6} [inst : Fintype ι] [inst_1 : DecidableEq ι] [inst_2 : CommRing R] (p : ENNReal)
  (m : Matrix ι ι R), LinearMap.det ((Matrix.toLpLin p p) m) = m.det
-- Mathlib.MeasureTheory.Measure.SeparableMeasure
/-- Any measurable set can be approximated by sets in the family.  -/
MeasureTheory.Measure.MeasureDense.approx : ∀ {X : Type u_1} [m : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝒜 : Set (Set X)},
  μ.MeasureDense 𝒜 →
    ∀ (s : Set X), MeasurableSet s → μ s ≠ ⊤ → ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ (symmDiff s t) < ENNReal.ofReal ε
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.comm_tmul : ∀ (R : Type u_1) [inst : CommSemiring R] (M : Type u_7) (N : Type u_8) [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (m : M) (n : N),
  (TensorProduct.comm R M N) (m ⊗ₜ[R] n) = n ⊗ₜ[R] m
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
hasLineDerivWithinAt_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {s : Set E}
  {x : E}, HasLineDerivWithinAt 𝕜 f 0 s x 0
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
/-- A functor preserves effective epimorphisms if it maps effective
epimorphisms to effective epimorphisms.
 -/
CategoryTheory.Functor.PreservesEffectiveEpis.preserves : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {D : Type u_2}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {F : CategoryTheory.Functor C D} [self : F.PreservesEffectiveEpis]
  {X Y : C} (f : X ⟶ Y) [CategoryTheory.EffectiveEpi f], CategoryTheory.EffectiveEpi (F.map f)
-- Mathlib.Order.GaloisConnection.Basic
GaloisCoinsertion.u_biSup_l : ∀ {α : Type u} {β : Type v} {u : α → β} {l : β → α} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  (gi : GaloisCoinsertion l u) {ι : Sort x} {p : ι → Prop} (f : (i : ι) → p i → β),
  u (⨆ i, ⨆ (hi : p i), l (f i hi)) = ⨆ i, ⨆ (hi : p i), f i hi
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
coprime_card_of_isCyclic_prod : ∀ (M : Type u_4) (N : Type u_5) [inst : Group M] [inst_1 : Group N] [cyc : IsCyclic (M × N)] [Finite M] [Finite N],
  (Nat.card M).Coprime (Nat.card N)
-- Mathlib.Logic.Function.Basic
Function.apply_extend : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} {g : α → γ} (F : γ → δ) (f : α → β) (e' : β → γ) (b : β),
  F (Function.extend f g e' b) = Function.extend f (F ∘ g) (F ∘ e') b
-- Mathlib.Analysis.Convex.Intrinsic
AffineEquiv.intrinsicInterior_image : ∀ {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} {Q : Type u_4} {P : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [CompleteSpace 𝕜] [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V]
  [inst_5 : NormedAddCommGroup W] [inst_6 : NormedSpace 𝕜 W] [inst_7 : MetricSpace P] [inst_8 : NormedAddTorsor V P]
  [inst_9 : MetricSpace Q] [inst_10 : NormedAddTorsor W Q] (φ : P ≃ᵃ[𝕜] Q) (s : Set P),
  intrinsicInterior 𝕜 (⇑φ '' s) = ⇑φ '' intrinsicInterior 𝕜 s
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.top_subgroupOf : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), ⊤.subgroupOf H = ⊤
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.insertMany.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {ρ : Type w} [inst_1 : ForIn Id ρ ((a : α) × β a)]
  (t : Std.DTreeMap.Internal.Impl α β) (l : ρ) (h : t.Balanced),
  t.insertMany l h =
    (have r := ⟨t, ⋯⟩;
      do
      let __s ←
        forIn l r fun x __s =>
            let r := __s;
            match x with
            | ⟨a, b⟩ =>
              have hr := ⋯;
              have r := ⟨(Std.DTreeMap.Internal.Impl.insert a b (↑r) hr).impl, ⋯⟩;
              pure (ForInStep.yield r)
      have r : t.IteratedInsertionInto := __s
      pure r).run
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec64_ofInt : ∀ (i : ℤ) (h : System.Platform.numBits = 64), (ISize.ofInt i).toBitVec64 h = BitVec.ofInt 64 i
-- Mathlib.RingTheory.SurjectiveOnStalks
RingHom.surjectiveOnStalks_iff_of_isLocalHom : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {f : R →+* S} [IsLocalRing S] [IsLocalHom f],
  f.SurjectiveOnStalks ↔ Function.Surjective ⇑f
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.residue_eq_zero_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R] (x : R),
  (IsLocalRing.residue R) x = 0 ↔ x ∈ IsLocalRing.maximalIdeal R
-- Aesop.Tree.Data
Aesop.RappId.instToString : ToString Aesop.RappId
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.isLeast_opNorm : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι]
  (f : ContinuousMultilinearMap 𝕜 E G), IsLeast {c | 0 ≤ c ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ c * ∏ i, ‖m i‖} ‖f‖
-- Mathlib.Analysis.Normed.Group.Pointwise
/-- **Alias** of `infEDist_neg_neg`. -/
infEdist_neg_neg : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (x : E) (s : Set E), Metric.infEDist (-x) (-s) = Metric.infEDist x s
-- Mathlib.Algebra.Free
FreeSemigroup.traverse_mul : ∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β) [LawfulApplicative m]
  (x y : FreeSemigroup α), traverse F (x * y) = (fun x1 x2 => x1 * x2) <$> traverse F x <*> traverse F y
-- Mathlib.Tactic.DefEqTransformations
/-- For each fvar, looks for its body in `e` and replaces it with the fvar.  -/
Mathlib.Tactic.refoldFVars : Array Lean.FVarId → Option Lean.FVarId → Lean.Expr → Lean.MetaM Lean.Expr
-- Batteries.Data.String.Lemmas
String.revPosOfAux_eq : ∀ (s : String) (c : Char), String.Legacy.revPosOfAux s c = String.Legacy.revFindAux s fun x => x == c
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
/-- The Cech object of `U : FormalCoproduct C` has an extra degeneracy
when there is a morphism `T ⟶ U.obj i₀` from the terminal object.  -/
CategoryTheory.Limits.FormalCoproduct.extraDegeneracyCech : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] →
      (U : CategoryTheory.Limits.FormalCoproduct C) →
        {T : C} →
          (hT : CategoryTheory.Limits.IsTerminal T) →
            {i₀ : U.I} →
              (T ⟶ U.obj i₀) →
                (U.cech.augmentOfIsTerminal (CategoryTheory.Limits.FormalCoproduct.isTerminalIncl T hT)).ExtraDegeneracy
-- Mathlib.CategoryTheory.Category.Factorisation
/-- The midpoint of the factorisation.  -/
CategoryTheory.Factorisation.mid : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → {f : X ⟶ Y} → CategoryTheory.Factorisation f → C
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
AddGroup.isAddCyclic_of_coprime_card_range_card_ker : ∀ {M : Type u_4} {N : Type u_5} [inst : AddCommGroup M] [inst_1 : AddGroup N] (f : M →+ N),
  (Nat.card ↥f.ker).Coprime (Nat.card ↥f.range) → ∀ [IsAddCyclic ↥f.ker] [IsAddCyclic ↥f.range], IsAddCyclic M
-- Mathlib.RingTheory.Localization.AsSubring
/-- Given a domain `A` with fraction field `K`, and a submonoid `S` of `A` which
contains no zero divisor, this is the localization of `A` at `S`, considered as
a subalgebra of `K` over `A`.

The carrier of this subalgebra is defined as the set of all `x : K` of the form
`algebraMap A K a * (algebraMap A K s)⁻¹` where `a s : A` and `s ∈ S`.
 -/
Localization.subalgebra.ofField : {A : Type u_1} →
  (K : Type u_2) →
    [inst : CommRing A] →
      (S : Submonoid A) →
        S ≤ nonZeroDivisors A → [inst_1 : Field K] → [inst_2 : Algebra A K] → [IsFractionRing A K] → Subalgebra A K
-- Mathlib.RingTheory.Polynomial.Basic
Algebra.algHom.eq_1 : Algebra.algHom = IsScalarTower.toAlgHom
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
/-- If `c` is a fork in `Cᵒᵖ`, then `c.unop.op` is isomorphic to `c`.  -/
CategoryTheory.Limits.Fork.unopOpIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : Cᵒᵖ} → {f g : X ⟶ Y} → (c : CategoryTheory.Limits.Fork f g) → c.unop.op ≅ c
-- Mathlib.Algebra.Star.StarProjection
/-- `q - p` is a star projection when `p * q = p`.  -/
IsStarProjection.sub_of_mul_eq_left : ∀ {R : Type u_1} {p q : R} [inst : NonUnitalNonAssocRing R] [inst_1 : StarRing R],
  IsStarProjection p → IsStarProjection q → p * q = p → IsStarProjection (q - p)
-- Mathlib.LinearAlgebra.Dimension.Free
lift_rank_le_iff_exists_linearMap : ∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Free R M] [inst_4 : AddCommMonoid M'] [inst_5 : Module R M'] [Module.Free R M'] [StrongRankCondition R],
  Cardinal.lift.{v', v} (Module.rank R M) ≤ Cardinal.lift.{v, v'} (Module.rank R M') ↔ ∃ f, Function.Injective ⇑f
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzWith.prod_fst : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β], LipschitzWith 1 Prod.fst
-- Init.Data.BitVec.Lemmas
BitVec.ne_not_self : ∀ {w : ℕ} {a : BitVec w}, 0 < w → a ≠ ~~~a
-- Mathlib.Order.BoundedOrder.Basic
/-- Pullback an `OrderTop`.  -/
OrderTop.lift : {α : Type u} →
  {β : Type v} →
    [inst : LE α] →
      [inst_1 : Top α] →
        [inst_2 : LE β] → [inst_3 : OrderTop β] → (f : α → β) → (∀ (a b : α), f a ≤ f b → a ≤ b) → f ⊤ = ⊤ → OrderTop α
-- Mathlib.RingTheory.LocalProperties.Submodule
LinearMap.eq_of_localization_maximal : ∀ {R : Type u_1} {M : Type u_2} {M₁ : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5)
  [inst_5 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)]
  [inst_6 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Module R (Mₚ P)]
  (f : (P : Ideal R) → [inst_7 : P.IsMaximal] → M →ₗ[R] Mₚ P)
  [inst_7 : ∀ (P : Ideal R) [inst_7 : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)]
  (M₁ₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6)
  [inst_8 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (M₁ₚ P)]
  [inst_9 : (P : Ideal R) → [inst_9 : P.IsMaximal] → Module R (M₁ₚ P)]
  (f₁ : (P : Ideal R) → [inst_10 : P.IsMaximal] → M₁ →ₗ[R] M₁ₚ P)
  [inst_10 : ∀ (P : Ideal R) [inst_10 : P.IsMaximal], IsLocalizedModule P.primeCompl (f₁ P)] (g g' : M →ₗ[R] M₁),
  (∀ (P : Ideal R) [inst_11 : P.IsMaximal],
      (IsLocalizedModule.map P.primeCompl (f P) (f₁ P)) g = (IsLocalizedModule.map P.primeCompl (f P) (f₁ P)) g') →
    g = g'
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.carrierEquiv.eq_1 : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S},
  AlgebraicGeometry.Scheme.Pullback.carrierEquiv =
    {
      toFun := fun t =>
        ⟨AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint t, AlgebraicGeometry.Scheme.Pullback.SpecOfPoint t⟩,
      invFun := fun T => T.fst.SpecTensorTo T.snd, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- Compositional version of `Measurable.mul` for use by `fun_prop`.  -/
Measurable.mul' : ∀ {M : Type u_2} {α : Type u_3} {β : Type u_4} [inst : MeasurableSpace M] [inst_1 : Mul M] {m : MeasurableSpace α}
  {mβ : MeasurableSpace β} [MeasurableMul₂ M] {f g : α → β → M} {h : α → β},
  Measurable ↿f → Measurable ↿g → Measurable h → Measurable fun a => (f a * g a) (h a)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l →
        ∀ {h' : k' ∈ Std.ExtDTreeMap.Const.ofList l cmp}, (Std.ExtDTreeMap.Const.ofList l cmp).getKey k' h' = k
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
CategoryTheory.ObjectProperty.limitsClosure_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {α : Type t}
  {J : α → Type u'} [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)] {Q : CategoryTheory.ObjectProperty C}
  [Q.IsClosedUnderIsomorphisms] [∀ (a : α), Q.IsClosedUnderLimitsOfShape (J a)], P ≤ Q → P.limitsClosure J ≤ Q
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.ae_eq_mk : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} (hf : MeasureTheory.AEStronglyMeasurable f μ), f =ᵐ[μ] MeasureTheory.AEStronglyMeasurable.mk f hf
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.fst_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G H : CategoryTheory.AddGrp C),
  (CategoryTheory.SemiCartesianMonoidalCategory.fst G H).hom.hom =
    CategoryTheory.SemiCartesianMonoidalCategory.fst G.X H.X
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom₂.comp_app_assoc : ∀ {C D : CategoryTheory.Cat} {F G H : C ⟶ D} (α : F ⟶ G) (β : G ⟶ H) (X : ↑C) {Z : ↑D} (h : H.toFunctor.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp α β).toNatTrans.app X) h =
    CategoryTheory.CategoryStruct.comp (α.toNatTrans.app X) (CategoryTheory.CategoryStruct.comp (β.toNatTrans.app X) h)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_map_of_getKey?_eq_some : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [Std.TransOrd α] [inst : Inhabited γ] {f : α → β → γ} {k k' : α},
  t.WF →
    t.getKey? k = some k' →
      Std.DTreeMap.Internal.Impl.Const.get! (Std.DTreeMap.Internal.Impl.map f t) k =
        (Option.map (f k') (Std.DTreeMap.Internal.Impl.Const.get? t k)).get!
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.activateScoped : {α β σ : Type} → Lean.ScopedEnvExtension α β σ → Lean.Environment → Lean.Name → Lean.Environment
-- Mathlib.Data.Matrix.Mul
neg_dotProduct : ∀ {m : Type u_2} {α : Type v} [inst : Fintype m] [inst_1 : NonUnitalNonAssocRing α] (v w : m → α), -v ⬝ᵥ w = -(v ⬝ᵥ w)
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftComm_symm : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddCommMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (X : C) (i j : A),
  (CategoryTheory.shiftComm X i j).symm = CategoryTheory.shiftComm X j i
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey!_le_maxKey!_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {k : α} {v : β k}, (cmp t.maxKey! (t.insert k v).maxKey!).isLE = true
-- Mathlib.Algebra.Group.Defs
IsCancelMul.toIsLeftCancelMul : ∀ {G : Type u} {inst : Mul G} [self : IsCancelMul G], IsLeftCancelMul G
-- Mathlib.Topology.Compactness.SigmaCompact
exists_mem_compactCovering : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : SigmaCompactSpace X] (x : X), ∃ n, x ∈ compactCovering X n
-- Mathlib.Data.Set.Function
Set.EqOn.comp_left₂ : ∀ {α : Type u_7} {β : Type u_8} {δ : Type u_9} {γ : Type u_10} {op : α → β → δ} {a₁ a₂ : γ → α} {b₁ b₂ : γ → β}
  {s : Set γ}, Set.EqOn a₁ a₂ s → Set.EqOn b₁ b₂ s → Set.EqOn (fun x => op (a₁ x) (b₁ x)) (fun x => op (a₂ x) (b₂ x)) s
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- In a group with a left invariant measure `μ` and a right invariant measure `ν`, one can express
integrals with respect to `μ` as integrals with respect to `ν` up to a constant scaling factor
(given in the statement as `∫ x, g x ∂μ` where `g` is a fixed reference function) and an
explicit density `y ↦ 1/∫ z, g (z⁻¹ * y) ∂ν`.  -/
MeasureTheory.Measure.integral_isMulLeftInvariant_isMulRightInvariant_combo : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] [inst_3 : MeasurableSpace G]
  [BorelSpace G] {μ ν : MeasureTheory.Measure G} [MeasureTheory.IsFiniteMeasureOnCompacts μ]
  [MeasureTheory.IsFiniteMeasureOnCompacts ν] [μ.IsMulLeftInvariant] [ν.IsMulRightInvariant] [ν.IsOpenPosMeasure]
  {f g : G → ℝ},
  Continuous f →
    HasCompactSupport f →
      Continuous g →
        HasCompactSupport g →
          0 ≤ g →
            ∀ {x₀ : G},
              g x₀ ≠ 0 → ∫ (x : G), f x ∂μ = (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) * ∫ (x : G), g x ∂μ
-- Mathlib.Algebra.Order.Group.Abs
abs_add_eq_add_abs_iff : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] (a b : G),
  |a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
-- Mathlib.Data.Set.Lattice.Image
Set.iUnion₂_prod_const : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_8} {s : (i : ι) → κ i → Set α} {t : Set β},
  (⋃ i, ⋃ j, s i j) ×ˢ t = ⋃ i, ⋃ j, s i j ×ˢ t
-- Std.Do.Triple.SpecLemmas
modifyGetThe.eq_1 : ∀ {α : Type u} (σ : Type u) {m : Type u → Type v} [inst : MonadStateOf σ m] (f : σ → α × σ),
  modifyGetThe σ f = MonadStateOf.modifyGet f