mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Projectivization.Subspace
/-- The span of a set of points is contained in a subspace if and only if the set of points is
contained in the subspace.  -/
Projectivization.Subspace.span_le_subspace_iff : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {S : Set (Projectivization K V)} {W : Projectivization.Subspace K V}, Projectivization.Subspace.span S ≤ W ↔ S ⊆ ↑W
-- Init.Sym.DSimp.DSimprocDSL
/-- Maximum number of simplification steps.  -/
Lean.Parser.Command.symDSimpFieldMaxSteps : Lean.ParserDescr
-- Init.Data.Int.Lemmas
Int.add_left_comm : ∀ (a b c : ℤ), a + (b + c) = b + (a + c)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_alter_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {f : Option β → Option β}, (t.alter k f)[k]? = f t[k]?
-- Mathlib.Data.Set.Prod
Set.range_diag : ∀ {α : Type u_1}, Set.range Function.diag = Set.diagonal α
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get_insertMany_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {l : List α} {k k' : α},
      cmp k k' = Ordering.eq →
        ∀ {h' : k' ∈ t.insertMany l},
          k ∉ t → List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (t.insertMany l).get k' h' = k
-- Std.Data.Iterators.Lemmas.Equivalence.StepCongr
Std.IterM.QuotStep.transportAlongEquiv : {α₁ : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β α₂ : Type u_1} →
      [inst : Std.Iterator α₁ m β] →
        [inst_1 : Std.Iterator α₂ m β] →
          [inst_2 : Monad m] →
            [inst_3 : LawfulMonad m] →
              {ita : Std.IterM m β} → {itb : Std.IterM m β} → ita.Equiv itb → ita.QuotStep → itb.QuotStep
-- Mathlib.CategoryTheory.Functor.EpiMono
/-- A functor reflects epimorphisms if morphisms that are mapped to epimorphisms are themselves
epimorphisms.  -/
CategoryTheory.Functor.ReflectsEpimorphisms : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.instReprCustomEliminators.repr : Lean.Meta.CustomEliminators → ℕ → Std.Format
-- Init.Data.UInt.Lemmas
instLawfulIdentityUInt32HAddOfNat : Std.LawfulIdentity (fun x1 x2 => x1 + x2) 0
-- Mathlib.Topology.EMetricSpace.BoundedVariation
eVariationOn.locallyBoundedVariation_ofDual : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α},
  LocallyBoundedVariationOn (f ∘ ⇑OrderDual.ofDual) (⇑OrderDual.ofDual ⁻¹' s) ↔ LocallyBoundedVariationOn f s
-- Mathlib.Data.Fintype.BigOperators
Fintype.prod_eq_single : ∀ {α : Type u_1} {M : Type u_4} [inst : Fintype α] [inst_1 : CommMonoid M] {f : α → M} (a : α),
  (∀ (x : α), x ≠ a → f x = 1) → ∏ x, f x = f a
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.biprod_inr_fst_f : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} (K L : HomologicalComplex C c)
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] (i : ι),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inr.f i) (CategoryTheory.Limits.biprod.fst.f i) = 0
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.smul_congr : ∀ {R : Type u_2} {α : Type u_3} [inst : CommSemiring α] [inst_1 : SMul R α] {r : R} {a b t c : α},
  a = b → (∀ (x : α), r • x = t * x) → t * b = c → r • a = c
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
/-- If the product of bounded continuous functions is zero, then the norm of their sum is the
maximum of their norms.  -/
BoundedContinuousFunction.nnnorm_add_eq_max : ∀ {α : Type u} [inst : TopologicalSpace α] {R : Type u_1} [inst_1 : NonUnitalSeminormedRing R] [IsCancelMulZero R]
  {f g : BoundedContinuousFunction α R}, f * g = 0 → ‖f + g‖₊ = max ‖f‖₊ ‖g‖₊
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives
CategoryTheory.LocalizerMorphism.Derives.hasPointwiseRightDerivedFunctor : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} H]
  {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂}
  {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {F : CategoryTheory.Functor C₂ H},
  Φ.Derives F → ∀ [Φ.IsRightDerivabilityStructure], F.HasPointwiseRightDerivedFunctor W₂
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.comap_inf : ∀ {α : Type u_2} {β : Type u_3} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β] (L M : BooleanSubalgebra β)
  (f : BoundedLatticeHom α β),
  BooleanSubalgebra.comap f (L ⊓ M) = BooleanSubalgebra.comap f L ⊓ BooleanSubalgebra.comap f M
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
_private.Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense.0.CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.lift.congr_simp : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] {data : (X : C) → F.OneHypercoverDenseData J₀ J X}
  {G : CategoryTheory.Functor Cᵒᵖ A} (hG₀ : CategoryTheory.Presheaf.IsSheaf J₀ (F.op.comp G))
  (hG hG_1 : (X : C) → CategoryTheory.Limits.IsLimit ((data X).toOneHypercover.multifork G)),
  hG = hG_1 →
    ∀ {X : C} {S : J.Cover X} (s : CategoryTheory.Limits.Multifork (S.index G)),
      CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.lift✝ hG₀ hG s =
        CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.lift✝ hG₀ hG_1 s
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.tendsto_measure_Ici_atBot : ∀ {α : Type u_1} {m0 : MeasurableSpace α} [inst : Preorder α] [Filter.atBot.IsCountablyGenerated]
  (μ : MeasureTheory.Measure α), Filter.Tendsto (fun x => μ (Set.Ici x)) Filter.atBot (nhds (μ Set.univ))
-- Mathlib.Tactic.Linter.OverlappingInstances
/-- Compute the parent classes of `cls`, excluding parent classes that have a parent themselves.
The reason to exclude such classes is that if there is a duplication in such a class,
then there will necessarily also be a duplication in its parent.
If `cls` carries data, then only consider parents that carry data.
If `cls` is a non-structure class, this simply returns `#[cls]`.

The resulting expressions contain bound variables that correspond to the parameters of `cls`.
The universe levels and bound variables need to be instantiated to get concrete data projections.  -/
_private.Mathlib.Tactic.Linter.OverlappingInstances.0.Mathlib.Linter.OverlappingInstances.getAbstractProjections : Lean.Name → Lean.CoreM (Array Lean.Expr)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.d_step1_certC : Lean.Grind.CommRing.Poly → ℤ → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → ℕ → Bool
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_alter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k k' : α}
  [hi : Inhabited (β k')] {f : Option (β k) → Option (β k)},
  (m.alter k f).get! k' = if heq : (k == k') = true then (Option.map (cast ⋯) (f (m.get? k))).get! else m.get! k'
-- Mathlib.FieldTheory.Perfect
iterateFrobeniusEquiv_eq_pow : ∀ (R : Type u_1) (p n : ℕ) [inst : CommSemiring R] [inst_1 : ExpChar R p] [inst_2 : PerfectRing R p],
  iterateFrobeniusEquiv R p n = frobeniusEquiv R p ^ n
-- Mathlib.Algebra.Homology.Additive
CategoryTheory.instPreservesZeroMorphismsHomologicalComplexMapHomologicalComplex : ∀ {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [inst : CategoryTheory.Category.{v_2, u_3} W₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_4} W₂] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms W₁]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms W₂] (F : CategoryTheory.Functor W₁ W₂)
  [inst_4 : F.PreservesZeroMorphisms] (c : ComplexShape ι), (F.mapHomologicalComplex c).PreservesZeroMorphisms
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.coe_of_orthogonal_eq_bot_mk : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] {v : ι → E} (hon : Orthonormal 𝕜 v)
  (hsp : (Submodule.span 𝕜 (Set.range v))ᗮ = ⊥), ⇑(OrthonormalBasis.mkOfOrthogonalEqBot hon hsp) = v
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
/-- The group structure on `QuaternionGroup n`.
 -/
QuaternionGroup.instGroup : {n : ℕ} → Group (QuaternionGroup n)
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.W : Std.Time.GenericFormat.DateBuilder✝ → Option Std.Time.Week.Ordinal
-- Mathlib.Algebra.Group.Commute.Defs
Commute.mul_pow : ∀ {M : Type u_2} [inst : Monoid M] {a b : M}, Commute a b → ∀ (n : ℕ), (a * b) ^ n = a ^ n * b ^ n
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.weightedSMul_add_measure : ∀ {α : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {m : MeasurableSpace α}
  (μ ν : MeasureTheory.Measure α) {s : Set α},
  μ s ≠ ⊤ →
    ν s ≠ ⊤ → MeasureTheory.weightedSMul (μ + ν) s = MeasureTheory.weightedSMul μ s + MeasureTheory.weightedSMul ν s
-- Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
CategoryTheory.TwoSquare.GuitartExact.hComp' : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃]
  {V₁ : CategoryTheory.Functor C₁ D₁} {T₁ : CategoryTheory.Functor C₁ C₂} {B₁ : CategoryTheory.Functor D₁ D₂}
  {V₂ : CategoryTheory.Functor C₂ D₂} (w : CategoryTheory.TwoSquare T₁ V₁ V₂ B₁) {T₂ : CategoryTheory.Functor C₂ C₃}
  {B₂ : CategoryTheory.Functor D₂ D₃} {V₃ : CategoryTheory.Functor C₃ D₃} (w' : CategoryTheory.TwoSquare T₂ V₂ V₃ B₂)
  {T₁₂ : CategoryTheory.Functor C₁ C₃} {B₁₂ : CategoryTheory.Functor D₁ D₃} (eT : T₁.comp T₂ ≅ T₁₂)
  (eB : B₁.comp B₂ ≅ B₁₂) [w.GuitartExact] [w'.GuitartExact], (w.hComp' w' eT eB).GuitartExact
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.single_eq_of_ne : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → Zero (G i)] [inst_3 : ∀ (i : ι), ZeroMemClass (S i) (G i)] {i j : ι}
  (r : G i), j ≠ i → (RestrictedProduct.single A i r) j = 0
-- Mathlib.RingTheory.Coprime.Lemmas
Fintype.prod_dvd_of_isRelPrime : ∀ {α : Type u_2} {I : Type u_1} [inst : CommMonoid α] [DecompositionMonoid α] {z : α} {s : I → α} [inst_2 : Fintype I],
  Pairwise (Function.onFun IsRelPrime s) → (∀ (i : I), s i ∣ z) → ∏ x, s x ∣ z
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
SimpleGraph.IsPathGraph3Compl.mk : ∀ {α : Type u} {G : SimpleGraph α} {v w₁ w₂ : α}, G.Adj w₁ w₂ → ¬G.Adj v w₁ → ¬G.Adj v w₂ → G.IsPathGraph3Compl v w₁ w₂
-- Mathlib.Algebra.Star.Basic
/-- Any commutative monoid admits the trivial \*-structure.

See note [reducible non-instances].
 -/
starMulOfComm : {R : Type u_1} → [inst : CommMonoid R] → StarMul R
-- Mathlib.RingTheory.PolynomialLaw.Basic
/-- The auxiliary lift of `PolynomialLaw.toFun'` on `PolynomialLaw.lifts`  -/
PolynomialLaw.toFunLifted : {R : Type u} →
  [inst : CommSemiring R] →
    {M : Type u_1} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_2} →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] →
                (S : Type v) →
                  [inst_5 : CommSemiring S] →
                    [inst_6 : Algebra R S] → (M →ₚₗ[R] N) → PolynomialLaw.lifts R M S → TensorProduct R S N
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.ofIso_N : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : CategoryTheory.SimplicialObject C}
  (s : X.Splitting) (e : X ≅ Y) (a : ℕ), (s.ofIso e).N a = s.N a
-- Mathlib.LinearAlgebra.Complex.Module
Complex.instSMulCommClassOfReal : ∀ {R : Type u_1} {S : Type u_2} [inst : SMul R ℝ] [inst_1 : SMul S ℝ] [SMulCommClass R S ℝ], SMulCommClass R S ℂ
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.mem_toAddSubgroup : ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] {module_M : Module R M} (p : Submodule R M)
  {x : M}, x ∈ p.toAddSubgroup ↔ x ∈ p
-- Mathlib.Algebra.BigOperators.Finprod
/-- **Alias** of `finsum_cond_pos`. -/
finprod_cond_pos : ∀ {ι : Type u_3} {M : Type u_7} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelAddMonoid M]
  {f : ι → M} {p : ι → Prop},
  (∀ (i : ι), p i → 0 ≤ f i) →
    (∃ i, p i ∧ 0 < f i) → (Function.support f ∩ {i | p i}).Finite → 0 < ∑ᶠ (i : ι) (_ : p i), f i
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instNegZeroClassOfAddOpposite.eq_1 : ∀ {M : Type u_1} [inst : NegZeroClass Mᵃᵒᵖ], DomAddAct.instNegZeroClassOfAddOpposite = inst
-- Lean.Meta.HaveTelescope
_private.Lean.Meta.HaveTelescope.0.Lean.Meta.HaveTelescopeInfo.computeFixedUsed.go : Lean.Meta.HaveTelescopeInfo → Std.HashSet ℕ → Lean.MetaM (Array Bool)
-- Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound
_private.Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound.0.Std.Tactic.BVDecide.LRAT.Internal.lratChecker.match_3.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : List (Std.Tactic.BVDecide.LRAT.Action β α) → Sort u_3)
  (h_1 : Unit → motive [])
  (h_2 :
    (id : ℕ) →
      (rupHints : Array ℕ) →
        (tail : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
          motive (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints :: tail))
  (h_3 :
    (id : ℕ) →
      (c : β) →
        (rupHints : Array ℕ) →
          (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
            motive (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints :: restPrf))
  (h_4 :
    (id : ℕ) →
      (c : β) →
        (pivot : Std.Sat.Literal α) →
          (rupHints : Array ℕ) →
            (ratHints : Array (ℕ × Array ℕ)) →
              (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
                motive (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints :: restPrf))
  (h_5 :
    (ids : Array ℕ) →
      (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
        motive (Std.Tactic.BVDecide.LRAT.Action.del ids :: restPrf)),
  (match [] with
    | [] => h_1 ()
    | Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints :: tail => h_2 id rupHints tail
    | Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints :: restPrf => h_3 id c rupHints restPrf
    | Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints :: restPrf =>
      h_4 id c pivot rupHints ratHints restPrf
    | Std.Tactic.BVDecide.LRAT.Action.del ids :: restPrf => h_5 ids restPrf) =
    h_1 ()
-- Mathlib.Analysis.LocallyConvex.SeparatingDual
SeparatingDual.t2Space : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : TopologicalSpace V]
  [inst_3 : TopologicalSpace R] [inst_4 : Module R V] [SeparatingDual R V] [T2Space R], T2Space V
-- Init.Data.Rat.Lemmas
Rat.neg_lt_neg : ∀ {a b : ℚ}, a < b → -b < -a
-- Init.Data.String.Subslice
String.Slice.subslice!_eq_subslice : ∀ {s : String.Slice} {newStart newEnd : s.Pos} (h : newStart ≤ newEnd),
  s.subslice! newStart newEnd = s.subslice newStart newEnd h
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.areaForm_neg_orientation : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)), (-o).areaForm = -o.areaForm
-- Mathlib.Analysis.Normed.Group.Continuity
tendsto_norm_sub_self_nhdsNE : ∀ {E : Type u_7} [inst : NormedAddCommGroup E] (a : E),
  Filter.Tendsto (fun x => ‖x - a‖) (nhdsWithin a {a}ᶜ) (nhdsWithin 0 (Set.Ioi 0))
-- Aesop.Tree.Data
Aesop.Goal.setNormalizationState : Aesop.NormalizationState → Aesop.Goal → Aesop.Goal
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioi_union_Iic_of_le : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, b ≤ a → Set.Ioi b ∪ Set.Iic a = Set.univ
-- Mathlib.Computability.RegularExpressions
RegularExpression.rmatch.eq_def : ∀ {α : Type u_1} [inst : DecidableEq α] (x : RegularExpression α) (x_1 : List α),
  x.rmatch x_1 =
    match x, x_1 with
    | P, [] => P.matchEpsilon
    | P, a :: as => (P.deriv a).rmatch as
-- Batteries.Data.Fin.Lemmas
Fin.map_findSomeRev? : ∀ {n : ℕ} {α : Type u_1} {β : Type u_2} (f : Fin n → Option α) (g : α → β),
  Option.map g (Fin.findSomeRev? f) = Fin.findSomeRev? fun x => Option.map g (f x)
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.mul_invSelf : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (x : R)
  [inst_3 : IsLocalization.Away x S], (algebraMap R S) x * IsLocalization.Away.invSelf x = 1
-- Init.Data.Fin.Lemmas
Fin.ofNat_mul : ∀ {n : ℕ} [inst : NeZero n] (x : ℕ) (y : Fin n), Fin.ofNat n x * y = Fin.ofNat n (x * ↑y)
-- Mathlib.Algebra.GroupWithZero.Units.Basic
Units.mk0_inj : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b : G₀} (ha : a ≠ 0) (hb : b ≠ 0),
  Units.mk0 a ha = Units.mk0 b hb ↔ a = b
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.coeff_zero_iff : ∀ {σ : Type u_1} {τ : Type u_4} {S : Type u_5} [inst : CommRing S] {a : σ → MvPowerSeries τ S}
  [inst_1 : TopologicalSpace S] [DiscreteTopology S],
  Filter.Tendsto a Filter.cofinite (nhds 0) ↔ ∀ (d : τ →₀ ℕ), {s | (MvPowerSeries.coeff d) (a s) ≠ 0}.Finite
-- Mathlib.Algebra.Algebra.Basic
LinearEquiv.extendScalarsOfSurjective_apply : ∀ {R : Type u_1} {S : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M : Type u_2}
  {N : Type u_3} [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N] [inst_5 : Module R M] [inst_6 : Module S M]
  [inst_7 : IsScalarTower R S M] [inst_8 : Module R N] [inst_9 : Module S N] [inst_10 : IsScalarTower R S N]
  (h : Function.Surjective ⇑(algebraMap R S)) (f : M ≃ₗ[R] N) (x : M),
  (LinearEquiv.extendScalarsOfSurjective h f) x = f x
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
/-- `P` is a sheaf for `Presieve.ofArrows X π`, iff the fork given by `w` is an equalizer.  -/
CategoryTheory.Equalizer.Presieve.Arrows.sheaf_condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C} {I : Type t}
  [inst_1 : Small.{w, t} I] (X : I → C) (π : (i : I) → X i ⟶ B)
  [inst_2 : (CategoryTheory.Presieve.ofArrows X π).HasPairwisePullbacks],
  CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.ofArrows X π) ↔
    Nonempty
      (CategoryTheory.Limits.IsLimit
        (CategoryTheory.Limits.Fork.ofι (CategoryTheory.Equalizer.Presieve.Arrows.forkMap P X π) ⋯))
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_some : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  (hx : AlgebraicIndependent R x) (i : ι),
  hx.mvPolynomialOptionEquivPolynomialAdjoin (MvPolynomial.X (some i)) = Polynomial.C (hx.aevalEquiv (MvPolynomial.X i))
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
/-- Given a bounded bilinear map `f`, the map associating to a point `p` the derivative of `f` at
`p` is itself a bounded linear map.  -/
IsBoundedBilinearMap.isBoundedLinearMap_deriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {G : Type u_4} [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E × F → G}
  (h : IsBoundedBilinearMap 𝕜 f), IsBoundedLinearMap 𝕜 fun p => h.deriv p
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Comma.limitAuxiliaryCone_pt : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {A : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  {B : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃}
  [inst_3 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T}
  (F : CategoryTheory.Functor J (CategoryTheory.Comma L R))
  (c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R))),
  (CategoryTheory.Comma.limitAuxiliaryCone F c₁).pt = L.obj c₁.pt
-- Init.Data.Vector.Lemmas
Vector.getElem?_setIfInBounds_self_of_lt : ∀ {α : Type u_1} {n i : ℕ} {xs : Vector α n} {x : α}, i < n → (xs.setIfInBounds i x)[i]? = some x
-- Mathlib.Analysis.InnerProductSpace.l2Space
HilbertBasis.ofRepr.inj : ∀ {ι : Type u_1} {𝕜 : Type u_2} {inst : RCLike 𝕜} {E : Type u_3} {inst_1 : NormedAddCommGroup E}
  {inst_2 : InnerProductSpace 𝕜 E} {repr repr_1 : E ≃ₗᵢ[𝕜] ↥(lp (fun x => 𝕜) 2)},
  { repr := repr } = { repr := repr_1 } → repr = repr_1
-- Mathlib.Algebra.Module.Submodule.Range
/-- Restrict the codomain of a linear map `f` to `f.range`.

This is the bundled version of `Set.rangeFactorization`.  -/
LinearMap.rangeRestrict : {R : Type u_1} →
  {R₂ : Type u_2} →
    {M : Type u_5} →
      {M₂ : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R₂ M₂] →
                    {τ₁₂ : R →+* R₂} → [inst_6 : RingHomSurjective τ₁₂] → (f : M →ₛₗ[τ₁₂] M₂) → M →ₛₗ[τ₁₂] ↥f.range
-- Lean.Elab.Binders
_private.Lean.Elab.Binders.0.Lean.Elab.Term.elabBindersAux.loop : {α : Type} →
  Array Lean.Syntax →
    (Array (Lean.Syntax × Lean.Expr) → Lean.Elab.TermElabM α) →
      ℕ → Array (Lean.Syntax × Lean.Expr) → Lean.Elab.TermElabM α
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.conv_eq_withDensity_lconvolution_rnDeriv : ∀ {G : Type u_3} [inst : AddGroup G] {mG : MeasurableSpace G} [MeasurableAdd₂ G] [MeasurableNeg G]
  {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant] [MeasureTheory.SFinite μ] {ν₁ ν₂ : MeasureTheory.Measure G}
  [ν₁.HaveLebesgueDecomposition μ] [ν₂.HaveLebesgueDecomposition μ],
  ν₁.AbsolutelyContinuous μ →
    ν₂.AbsolutelyContinuous μ → ν₁.conv ν₂ = μ.withDensity (MeasureTheory.lconvolution (ν₁.rnDeriv μ) (ν₂.rnDeriv μ) μ)
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.ι_fromGlued_assoc : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.I₀) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Cover.gluedCover 𝒰).ι x)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.fromGlued 𝒰) h) =
    CategoryTheory.CategoryStruct.comp (𝒰.f x) h
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.mk_coe : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] (f : P →ᴬ[R] Q)
  (h : Continuous (↑f).toFun), { toAffineMap := ↑f, cont := h } = f
-- Init.Data.Array.Lemmas
/-- Variant of `getElem?_reverse` with a hypothesis giving the linear relation between the indices.  -/
Array.getElem?_reverse' : ∀ {α : Type u_1} {xs : Array α} {i j : ℕ}, i + j + 1 = xs.size → xs.reverse[i]? = xs[j]?
-- Init.Data.Vector.Lemmas
Vector.mem_set : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} {a : α} (hi : i < n), a ∈ xs.set i a hi
-- Mathlib.Algebra.BigOperators.NatAntidiagonal
Finset.Nat.prod_antidiagonal_subst : ∀ {M : Type u_1} [inst : CommMonoid M] {n : ℕ} {f : ℕ × ℕ → ℕ → M},
  ∏ p ∈ Finset.HasAntidiagonal.antidiagonal n, f p n = ∏ p ∈ Finset.HasAntidiagonal.antidiagonal n, f p (p.1 + p.2)