mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.MetavarContext
/-- Create a new `LocalContext` by removing the free variables in `toRevert` from `lctx`.
We use this function when we create auxiliary metavariables at `elimMVarDepsAux`.  -/
Lean.MetavarContext.MkBinding.reduceLocalContext : Lean.LocalContext → Array Lean.Expr → Lean.LocalContext
-- Lean.Meta.Tactic.Grind.AC.Util
_private.Lean.Meta.Tactic.Grind.AC.Util.0.Lean.Meta.Grind.AC.insertOpId.go : ℕ → List ℕ → List ℕ
-- Mathlib.Algebra.Order.Monovary
AntivaryOn.div_left₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : LinearOrder β] {s : Set ι} {f₁ f₂ : ι → α} {g : ι → β},
  (∀ i ∈ s, 0 ≤ f₁ i) → (∀ i ∈ s, 0 < f₂ i) → AntivaryOn f₁ g s → MonovaryOn f₂ g s → AntivaryOn (f₁ / f₂) g s
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toListRev_filterMapM : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [inst_4 : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {f : β → m (Option γ)}
  (it : Std.IterM Id β), (Std.IterM.filterMapM f it).toListRev = List.reverse <$> List.filterMapM f it.toList.run
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Presieve.factorsThru_top : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : C} (S : CategoryTheory.Presieve X), S.FactorsThru ⊤
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.IsCharThreeJNeZeroNF.a₁ : ∀ {R : Type u_1} {inst : CommRing R} {W : WeierstrassCurve R} [self : W.IsCharThreeJNeZeroNF], W.a₁ = 0
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
/-- The boxes in a prepartition are pairwise disjoint.  -/
BoxIntegral.Prepartition.pairwiseDisjoint : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (self : BoxIntegral.Prepartition I),
  (↑self.boxes).Pairwise (Function.onFun Disjoint BoxIntegral.Box.toSet)
-- Mathlib.Algebra.AlgebraicCard
Algebraic.cardinalMk_lift_of_infinite : ∀ (R : Type u) (A : Type v) [inst : CommRing R] [IsDomain R] [inst_2 : CommRing A] [IsDomain A] [inst_4 : Algebra R A]
  [Module.IsTorsionFree R A] [Infinite R],
  Cardinal.lift.{u, v} (Cardinal.mk { x // IsAlgebraic R x }) = Cardinal.lift.{v, u} (Cardinal.mk R)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.slope_of_Y_ne_eq_evalEval : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] {x₁ x₂ y₁ y₂ : F},
  x₁ = x₂ →
    y₁ ≠ W.negY x₂ y₂ →
      W.slope x₁ x₂ y₁ y₂ = -Polynomial.evalEval x₁ y₁ W.polynomialX / Polynomial.evalEval x₁ y₁ W.polynomialY
-- Mathlib.Data.Finset.Powerset
/-- When `s` is a finset, `s.powerset` is the finset of all subsets of `s` (seen as finsets).  -/
Finset.powerset : {α : Type u_1} → Finset α → Finset (Finset α)
-- Mathlib.RingTheory.Coalgebra.Basic
Coalgebra.Repr.mk.inj : ∀ {R : Type u} {A : Type v} {inst : CommSemiring R} {inst_1 : AddCommMonoid A} {inst_2 : Module R A}
  {inst_3 : CoalgebraStruct R A} {a : A} {ι : Type u_1} {index : Finset ι} {left right : ι → A}
  {eq : ∑ i ∈ index, left i ⊗ₜ[R] right i = CoalgebraStruct.comul a} {index_1 : Finset ι} {left_1 right_1 : ι → A}
  {eq_1 : ∑ i ∈ index_1, left_1 i ⊗ₜ[R] right_1 i = CoalgebraStruct.comul a},
  { index := index, left := left, right := right, eq := eq } =
      { index := index_1, left := left_1, right := right_1, eq := eq_1 } →
    index = index_1 ∧ left = left_1 ∧ right = right_1
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.Disjoint.mul_left : ∀ {α : Type u_1} {f g h : Equiv.Perm α}, f.Disjoint h → g.Disjoint h → (f * g).Disjoint h
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RciSliceData.range : {α : Type u} → {β : α → Type v} → [inst : Ord α] → Std.DTreeMap.Internal.RciSliceData α β → Std.Rci α
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
/-- The region between two measurable functions on a measurable set is measurable;
a version for the region together with the graph of the upper function.  -/
measurableSet_region_between_oc : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f g : α → ℝ} {s : Set α},
  Measurable f → Measurable g → MeasurableSet s → MeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Set.Ioc (f p.1) (g p.1)}
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.lieSpan_le : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {s : Set L}
  {K : LieSubalgebra R L}, LieSubalgebra.lieSpan R L s ≤ K ↔ s ⊆ ↑K
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.MkTableKey.State.mk.injEq : ∀ (nextIdx : ℕ) (lmap : Std.HashMap Lean.LMVarId Lean.Level) (emap : Std.HashMap Lean.MVarId Lean.Expr)
  (mctx : Lean.MetavarContext) (nextIdx_1 : ℕ) (lmap_1 : Std.HashMap Lean.LMVarId Lean.Level)
  (emap_1 : Std.HashMap Lean.MVarId Lean.Expr) (mctx_1 : Lean.MetavarContext),
  ({ nextIdx := nextIdx, lmap := lmap, emap := emap, mctx := mctx } =
      { nextIdx := nextIdx_1, lmap := lmap_1, emap := emap_1, mctx := mctx_1 }) =
    (nextIdx = nextIdx_1 ∧ lmap = lmap_1 ∧ emap = emap_1 ∧ mctx = mctx_1)
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.cancelBaseChange_tmul : ∀ (R : Type uR) (S : Type uS) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (T : Type u_3)
  (A : Type u_4) (B : Type u_5) [inst_3 : CommSemiring T] [inst_4 : CommSemiring A] [inst_5 : CommSemiring B]
  [inst_6 : Algebra R T] [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : Algebra T A]
  [inst_10 : IsScalarTower R T A] [inst_11 : Algebra S A] [inst_12 : IsScalarTower R S A] [inst_13 : Algebra S T]
  [inst_14 : IsScalarTower S T A] (a : A) (s : S) (b : B),
  (Algebra.TensorProduct.cancelBaseChange R S T A B) (a ⊗ₜ[S] (s ⊗ₜ[R] b)) = (s • a) ⊗ₜ[R] b
-- Mathlib.MeasureTheory.Function.Holder
MeasureTheory.Lp.smul_def : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p q r : ENNReal}
  [hpqr : p.HolderTriple q r] [inst : NormedRing 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : MulActionWithZero 𝕜 E]
  [inst_3 : IsBoundedSMul 𝕜 E] {f : ↥(MeasureTheory.Lp 𝕜 p μ)} {g : ↥(MeasureTheory.Lp E q μ)},
  f • g = MeasureTheory.MemLp.toLp (↑↑f • ↑↑g) ⋯
-- Batteries.Data.MLList.Basic
MLList.instAlternativeMonadOfMonad : {m : Type u_1 → Type u_1} → [Monad m] → AlternativeMonad (MLList m)
-- Mathlib.LinearAlgebra.Matrix.Invertible
/-- `Aᵀ` is invertible when `A` is.  -/
Matrix.invertibleOfInvertibleTranspose : {n : Type u_2} →
  {α : Type u_3} →
    [inst : Fintype n] →
      [inst_1 : DecidableEq n] →
        [inst_2 : CommSemiring α] → (A : Matrix n n α) → [Invertible A.transpose] → Invertible A
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.shouldShowMotive : Lean.Expr → Lean.Options → Lean.MetaM Bool
-- Lean.Meta.CongrTheorems
Lean.Meta.hcongrThmSuffixBasePrefix : String
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
/-- If `V` has a zero object, this is the functor from `V` to `Arrow V`
that sends an object `X` to the arrow `0 ⟶ X`.  -/
CategoryTheory.Preadditive.RightFreyd.rightFunctor : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [CategoryTheory.Preadditive V] →
      [CategoryTheory.Limits.HasZeroObject V] → CategoryTheory.Functor V (CategoryTheory.Arrow V)
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- The subshift defined by a family of forbidden patterns `F`.

This is a standard way to construct subshifts:
`MulSubshift.ofForbidden F` consists of all configurations `x : G → A` in which no pattern
`p ∈ F` occurs at any position.

Formally:
* the carrier is `forbidden F` (configurations avoiding `F`),
* it is closed because each occurrence set is open, and
* it is shift-invariant since avoidance is preserved by shifts.  -/
SymbolicDynamics.FullShift.MulSubshift.ofForbidden : {A : Type u_1} →
  [inst : TopologicalSpace A] →
    [inst_1 : Inhabited A] →
      {G : Type u_2} →
        [inst_2 : Monoid G] →
          [IsLeftCancelMul G] →
            [DiscreteTopology A] →
              Set (SymbolicDynamics.FullShift.Pattern A G) → SymbolicDynamics.FullShift.MulSubshift A G
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.finsetClopens.eq_1 : ∀ (X : Type u_2) [inst : TopologicalSpace X] [inst_1 : CompactSpace X] (d : DiscreteQuotient X),
  DiscreteQuotient.finsetClopens X d = (Set.range fun x => { carrier := d.proj ⁻¹' {x}, isClopen' := ⋯ }).toFinset
-- Lean.Meta.Basic
/-- If `e` is of the form `?m ...` instantiate metavars
 -/
Lean.Meta.instantiateMVarsIfMVarApp : Lean.Expr → Lean.MetaM Lean.Expr
-- Std.Http.Data.Request
Std.Http.Request.Head.mk.injEq : ∀ (method : Std.Http.Method) (version : Std.Http.Version) (uri : Std.Http.RequestTarget) (headers : Std.Http.Headers)
  (method_1 : Std.Http.Method) (version_1 : Std.Http.Version) (uri_1 : Std.Http.RequestTarget)
  (headers_1 : Std.Http.Headers),
  ({ method := method, version := version, uri := uri, headers := headers } =
      { method := method_1, version := version_1, uri := uri_1, headers := headers_1 }) =
    (method = method_1 ∧ version = version_1 ∧ uri = uri_1 ∧ headers = headers_1)
-- Mathlib.AlgebraicGeometry.Sites.Small
/-- **Alias** of `AlgebraicGeometry.Scheme.smallGrothendieckTopology_eq_toGrothendieck_smallPretopology`. -/
AlgebraicGeometry.Scheme.smallGrothendieckTopologyOfLE_eq_toGrothendieck_smallPretopology : ∀ {P Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme)
  [inst : P.IsStableUnderBaseChange] [inst_1 : P.IsMultiplicative] [inst_2 : P.RespectsIso]
  [inst_3 : Q.IsStableUnderComposition] [inst_4 : Q.IsStableUnderBaseChange] [inst_5 : Q.HasOfPostcompProperty Q],
  P ≤ Q →
    AlgebraicGeometry.Scheme.smallGrothendieckTopology P S =
      (AlgebraicGeometry.Scheme.smallPretopology P Q).toGrothendieck
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.Kind.nestedPRBC.sizeOf_spec : sizeOf Lean.Elab.Term.Do.ToTerm.Kind.nestedPRBC = 1
-- Init.Data.List.Scan.Lemmas
List.drop_scanr : ∀ {α : Type u_1} {β : Type u_2} {i : ℕ} {b : β} {l : List α} {f : α → β → β},
  i ≤ l.length → List.drop i (List.scanr f b l) = List.scanr f b (List.drop i l)
-- Mathlib.Order.Disjoint
Codisjoint.le_of_disjoint : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : BoundedOrder α] {a b c : α}, Codisjoint a b → Disjoint b c → c ≤ a
-- Mathlib.Analysis.Normed.Operator.Asymptotics
ContinuousLinearMap.isBigO_sub : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F)
  (l : Filter E) (x : E), (fun x' => f (x' - x)) =O[l] fun x' => x' - x
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue_cons_of_beq : ∀ {α : Type u} {β : Type v} [inst : BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} (h : (k == a) = true),
  Std.Internal.List.getValue a (⟨k, v⟩ :: l) ⋯ = v
-- Mathlib.GroupTheory.IsSubnormal
AddSubgroup.IsSubnormal.below.top : ∀ {G : Type u_2} [inst : AddGroup G] {motive : (a : AddSubgroup G) → a.IsSubnormal → Prop},
  AddSubgroup.IsSubnormal.below ⋯
-- Mathlib.RingTheory.OreLocalization.Basic
OreLocalization.neg_add_cancel : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : AddGroup X] [inst_3 : DistribMulAction R X] (x : OreLocalization S X), -x + x = 0
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- All supported expressions involving `BitVec` and operations on them.
 -/
Std.Tactic.BVDecide.BVExpr : ℕ → Type
-- Init.Data.Int.Gcd
Int.neg_lcm : ∀ {a b : ℤ}, (-a).lcm b = a.lcm b
-- Mathlib.Data.Sign.Defs
/-- `SignType.sign` respects strictly monotone zero-preserving maps.  -/
StrictMono.sign_comp : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : LinearOrder α] {β : Type u_2} {F : Type u_3} [inst_2 : Zero β]
  [inst_3 : Preorder β] [inst_4 : DecidableLT β] [inst_5 : FunLike F α β] [ZeroHomClass F α β] {f : F},
  StrictMono ⇑f → ∀ (a : α), SignType.sign (f a) = SignType.sign a
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Step.visit.injEq : ∀ (e e_1 : Lean.Meta.Simp.Result), (Lean.Meta.Simp.Step.visit e = Lean.Meta.Simp.Step.visit e_1) = (e = e_1)
-- Mathlib.Algebra.Order.Floor.Div
Nat.ceilDiv_eq_add_pred_div : ∀ (a b : ℕ), a ⌈/⌉ b = (a + b - 1) / b
-- Init.Omega.Constraint
/-- An exact constraint.  -/
Lean.Omega.Constraint.exact : ℤ → Lean.Omega.Constraint
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeExtension.mapValueGroupWithZero.eq_1 : ∀ (A : Type u_1) (B : Type u_2) [inst : CommRing A] [inst_1 : Ring B] [inst_2 : ValuativeRel A]
  [inst_3 : ValuativeRel B] [inst_4 : Algebra A B] [inst_5 : ValuativeExtension A B],
  ValuativeExtension.mapValueGroupWithZero A B =
    MonoidWithZeroHom.ValueGroup₀.embedding.comp
      (ValuativeRel.ValueGroupWithZero.orderMonoidIso
          (Valuation.comap (algebraMap A B) (ValuativeRel.valuation B))).toMonoidWithZeroHom
-- Mathlib.LinearAlgebra.Vandermonde
Matrix.det_vandermonde_eq_zero_iff : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} [IsDomain R] {v : Fin n → R},
  (Matrix.vandermonde v).det = 0 ↔ ∃ i j, v i = v j ∧ i ≠ j
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inv_inl : ∀ {R : Type u} {M : Type v} [inst : DivisionSemiring R] [inst_1 : AddCommGroup M] [inst_2 : Module Rᵐᵒᵖ M]
  [inst_3 : Module R M] (r : R), (TrivSqZeroExt.inl r)⁻¹ = TrivSqZeroExt.inl r⁻¹
-- Mathlib.Topology.MetricSpace.Kuratowski
/-- The Kuratowski embedding is an isometry.
Theorem 2.1 of [Assaf Naor, *Metric Embeddings and Lipschitz Extensions*][Naor-2015].  -/
kuratowskiEmbedding.isometry : ∀ (α : Type u) [inst : MetricSpace α] [inst_1 : TopologicalSpace.SeparableSpace α], Isometry (kuratowskiEmbedding α)
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.num_zero_NonnegCoeffs : (Lean.Grind.CommRing.Poly.num 0).NonnegCoeffs
-- Mathlib.Algebra.Group.Center
Set.one_mem_centralizer : ∀ {M : Type u_1} {S : Set M} [inst : MulOneClass M], 1 ∈ S.centralizer
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.Valid.next : ∀ {it : String.Legacy.Iterator}, it.Valid → it.hasNext = true → it.next.Valid
-- Lean.Class
/-- State of the type class environment extension.  -/
Lean.ClassState : Type
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.coe_ofLinearIsometry : ∀ {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₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (f : E →ₛₗᵢ[σ₁₂] E₂) (g : E₂ →ₛₗ[σ₂₁] E) (h₁ : f.toLinearMap ∘ₛₗ g = LinearMap.id)
  (h₂ : g ∘ₛₗ f.toLinearMap = LinearMap.id), ⇑(LinearIsometryEquiv.ofLinearIsometry f g h₁ h₂) = ⇑f
-- Init.ShareCommon
ShareCommonT.run : {m : Type u_1 → Type u_2} → {σ : ShareCommon.StateFactory} → {α : Type u_1} → [Monad m] → ShareCommonT σ m α → m α
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
/-- Given a path object `P` for `X`, two maps `f` and `g` in `X ⟶ Y`
are homotopic relative to `P` when there is a morphism `h : P.I ⟶ Y`
such that `P.i₀ ≫ h = f` and `P.i₁ ≫ h = g`.  -/
HomotopicalAlgebra.PathObject.RightHomotopy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] →
        HomotopicalAlgebra.PathObject Y → (X ⟶ Y) → (X ⟶ Y) → Type v
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.SearchStep.startPos_rejected : ∀ {s : String.Slice} {p q : s.Pos}, (String.Slice.Pattern.SearchStep.rejected p q).startPos = p
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.restrict_dirac_of_notMem : ∀ {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  {s : Set α} {x : α} {m : M}, x ∉ s → (MeasureTheory.VectorMeasure.dirac x m).restrict s = 0
-- Mathlib.Data.Analysis.Filter
Filter.Realizer.bot_σ : ∀ {α : Type u_1}, Filter.Realizer.bot.σ = Unit
-- Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
CategoryTheory.Presheaf.isSheaf_iff_of_isGeneratedByOneHypercovers : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] [J.IsGeneratedByOneHypercovers] (P : CategoryTheory.Functor Cᵒᵖ A),
  CategoryTheory.Presheaf.IsSheaf J P ↔
    ∀ ⦃X : C⦄ (E : J.OneHypercover X), Nonempty (CategoryTheory.Limits.IsLimit (E.multifork P))
-- Mathlib.Analysis.Meromorphic.Basic
/-- If `g` is meromorphic at `x`, then `f + g` is meromorphic at `x` if and only if `f` is meromorphic
at `x`.
 -/
MeromorphicAt.meromorphicAt_fun_add_iff_meromorphicAt₂ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f g : 𝕜 → E},
  MeromorphicAt g x → (MeromorphicAt (fun z => f z + g z) x ↔ MeromorphicAt f x)
-- Mathlib.RingTheory.Morita.Basic
/-- The underlying equivalence of categories  -/
MoritaEquivalence.eqv : {R : Type u₀} →
  [inst : CommSemiring R] →
    {A : Type u₁} →
      [inst_1 : Ring A] →
        [inst_2 : Algebra R A] →
          {B : Type u₂} →
            [inst_3 : Ring B] → [inst_4 : Algebra R B] → MoritaEquivalence R A B → (ModuleCat A ≌ ModuleCat B)
-- Mathlib.SetTheory.Lists
Lists'.cons'.inj : ∀ {α : Type u} {b : Bool} {a : Lists' α b} {a_1 : Lists' α true} {b_1 : Bool} {a_2 : Lists' α b_1}
  {a_3 : Lists' α true}, a.cons' a_1 = a_2.cons' a_3 → b = b_1 ∧ a ≍ a_2 ∧ a_1 = a_3
-- Mathlib.Data.List.Duplicate
List.duplicate_cons_self_iff : ∀ {α : Type u_1} {l : List α} {x : α}, List.Duplicate x (x :: l) ↔ x ∈ l
-- Mathlib.Data.Matrix.Composition
Matrix.comp_symm_transpose : ∀ {I : Type u_1} {J : Type u_2} {K : Type u_3} {L : Type u_4} {R : Type u_5} (M : Matrix (I × K) (J × L) R),
  (Matrix.comp J I L K R).symm M.transpose = (((Matrix.comp I J K L R).symm M).map fun x => x.transpose).transpose
-- Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
CategoryTheory.MorphismProperty.FunctorsInverting.comp_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {W : CategoryTheory.MorphismProperty C} {F₁ F₂ F₃ : W.FunctorsInverting D} (f : F₁ ⟶ F₂) (g : F₂ ⟶ F₃)
  {Z : CategoryTheory.Functor C D} (h : F₃.obj ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).hom h =
    CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp g.hom h)
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.containsThenInsertIfNew_fst_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} (h : m.WF) {a : α}
  {b : β a}, (m.containsThenInsertIfNew a b).1 = (Std.DHashMap.Internal.Raw₀.containsThenInsertIfNew ⟨m, ⋯⟩ a b).1
-- Qq.MetaM
Qq.MaybeLevelDefEq.notDefEq.sizeOf_spec : ∀ {u v : Lean.Level}, sizeOf Qq.MaybeLevelDefEq.notDefEq = 1
-- Mathlib.Order.Filter.Pointwise
Filter.addActionFilter.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : AddMonoid α] [inst_1 : AddAction α β],
  Filter.addActionFilter = { toVAdd := Filter.instVAddFilter, add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.RepresentationTheory.Rep.Basic
/-- Given a `k`-linear `G`-representation `(V, ρ)`, this is the representation defined by
restricting `ρ` to a `G`-invariant `k`-submodule of `V`.  -/
Rep.subrepresentation : {k : Type u} →
  {G : Type v} →
    [inst : Ring k] →
      [inst_1 : Monoid G] →
        (A : Rep.{u_1, u, v} k G) →
          (W : Submodule k ↑A) → (∀ (g : G), W ≤ Submodule.comap (A.ρ g) W) → Rep.{u_1, u, v} k G
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.liftTruncLE_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {X Y : C} (f : X ⟶ Y) (n : ℤ) [inst_6 : t.IsLE X n],
  CategoryTheory.CategoryStruct.comp (t.liftTruncLE f n) ((t.truncLEι n).app Y) = f
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
/-- Reduction step for matrices in `Δ m` which moves the matrices towards `reps`  -/
FixedDetMatrices.reduceStep : {m : ℤ} → FixedDetMatrix (Fin 2) ℤ m → FixedDetMatrix (Fin 2) ℤ m
-- Lean.Message
Lean.MessageData.brecOn.eq : ∀ {motive_1 : Lean.MessageData → Sort u} {motive_2 : Array Lean.MessageData → Sort u}
  {motive_3 : List Lean.MessageData → Sort u} (t : Lean.MessageData)
  (F_1 : (t : Lean.MessageData) → t.below → motive_1 t)
  (F_2 : (t : Array Lean.MessageData) → Lean.MessageData.below_1 t → motive_2 t)
  (F_3 : (t : List Lean.MessageData) → Lean.MessageData.below_2 t → motive_3 t),
  t.brecOn F_1 F_2 F_3 = F_1 t (Lean.MessageData.brecOn.go t F_1 F_2 F_3).2
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
LinearIsometryEquiv.lTensor_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (f : F ≃ₗᵢ[𝕜] G) (x : TensorProduct 𝕜 E F),
  (LinearIsometryEquiv.lTensor E f) x = (LinearEquiv.lTensor E f.toLinearEquiv) x
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.adjoin_eq_span : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] (s : Set A),
  (NonUnitalStarAlgebra.adjoin R s).toSubmodule = Submodule.span R ↑(Subsemigroup.closure (s ∪ star s))
-- Mathlib.RingTheory.Congruence.Hom
/-- `liftₐ` as an equivalence.  -/
RingCon.liftₐEquiv : {M : Type u_1} →
  {P : Type u_3} →
    {R : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring M] →
          [inst_2 : Algebra R M] →
            [inst_3 : Semiring P] →
              [inst_4 : Algebra R P] → (c : RingCon M) → { f // c ≤ RingCon.ker ↑f } ≃ (c.Quotient →ₐ[R] P)
-- Mathlib.Order.Interval.Basic
Interval.coe_injective : ∀ {α : Type u_1} [inst : LE α], Function.Injective Interval.coe
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → γ} {k fallback : α},
  (Std.ExtHashMap.map f m).getKeyD k fallback = m.getKeyD k fallback
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
HasProdLocallyUniformlyOn_euler_sin_prod : HasProdLocallyUniformlyOn (fun n z => 1 + sineTerm z n) (fun x => Complex.sin (↑Real.pi * x) / (↑Real.pi * x))
  Complex.integerComplement
-- Init.Prelude
/-- `default` is a function that produces a "default" element of any
`Inhabited` type. This element does not have any particular specified
properties, but it is often an all-zeroes value.  -/
Inhabited.default : {α : Sort u} → [self : Inhabited α] → α
-- Mathlib.Algebra.Ring.Prod
/-- Product of two distributive types is distributive.  -/
Prod.instDistrib : {R : Type u_1} → {S : Type u_3} → [Distrib R] → [Distrib S] → Distrib (R × S)
-- Std.Time.Duration
Std.Time.Duration.instCoeOffset_1 : Coe Std.Time.Second.Offset Std.Time.Duration
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.map_eq_iff : ∀ {ι : Type u_3} {α : ι → Type u_4} {β : ι → Type u_5} [inst : (i : ι) → AddCommMonoid (α i)]
  [inst_1 : (i : ι) → AddCommMonoid (β i)] (f : (i : ι) → α i →+ β i) (x y : DirectSum ι fun i => α i),
  (DirectSum.map f) x = (DirectSum.map f) y ↔ ∀ (i : ι), (f i) (x i) = (f i) (y i)
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.lowerCrossingTime_le_upperCrossingTime_succ : ∀ {Ω : Type u_1} {ι : Type u_2} [inst : ConditionallyCompleteLinearOrderBot ι] {a b : ℝ} {f : ι → Ω → ℝ} {N : ι} {n : ℕ}
  {ω : Ω}, MeasureTheory.lowerCrossingTime a b f N n ω ≤ MeasureTheory.upperCrossingTime a b f N (n + 1) ω