mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_left_cert.eq_1 : ∀ (p₁ p₂ : Int.Internal.Linear.Poly) (n : ℕ),
  Int.Internal.Linear.cooper_left_cert p₁ p₂ n =
    Int.Internal.Linear.Poly.casesOn p₁ (fun x => false) fun a x x_1 =>
      Int.Internal.Linear.Poly.casesOn p₂ (fun x => false) fun b y x_2 =>
        (Nat.beq x y).and' ((decide (a < 0)).and' ((decide (b > 0)).and' (n.beq a.natAbs)))
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.coe_one : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : One α], ↑1 = 1
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.FiniteMeasure.tendsto_normalize_testAgainstNN_of_tendsto : ∀ {Ω : Type u_1} [inst : Nonempty Ω] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.FiniteMeasure Ω}
  [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω] {γ : Type u_2} {F : Filter γ}
  {μs : γ → MeasureTheory.FiniteMeasure Ω},
  Filter.Tendsto μs F (nhds μ) →
    μ ≠ 0 →
      ∀ (f : BoundedContinuousFunction Ω NNReal),
        Filter.Tendsto (fun i => (μs i).normalize.toFiniteMeasure.testAgainstNN f) F
          (nhds (μ.normalize.toFiniteMeasure.testAgainstNN f))
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.mclosure_range : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F),
  AddSubmonoid.closure (Set.range ⇑f) = AddMonoidHom.mrange f
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.RightResolution.Hom.id_f : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  (R : Φ.RightResolution X₂),
  (CategoryTheory.LocalizerMorphism.RightResolution.Hom.id R).f = CategoryTheory.CategoryStruct.id R.X₁
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.sup_le : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] {f g h : E →ₛₗ.[σ] F}
  (H : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y), f ≤ h → g ≤ h → f.sup g H ≤ h
-- Mathlib.FieldTheory.SeparableDegree
Polynomial.natSepDegree_pow : ∀ {F : Type u} [inst : Field F] (f : Polynomial F) {n : ℕ}, (f ^ n).natSepDegree = if n = 0 then 0 else f.natSepDegree
-- Mathlib.Tactic.DepRewrite
/-- Apply `rewrite!` to a local declaration.  -/
Mathlib.Tactic.DepRewrite.depRewriteLocalDecl : Lean.Syntax → Bool → Lean.FVarId → optParam Mathlib.Tactic.DepRewrite.Config { } → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.RingTheory.Perfection
/-- The `p`-th root of an element of the perfection.  -/
Perfection.pthRootMonoidHom : (M : Type u_1) → [inst : CommMonoid M] → (p : ℕ) → Perfection M p →* Perfection M p
-- Mathlib.Algebra.Group.Units.Defs
/-- See Note [custom simps projection]  -/
AddUnits.Simps.val_neg : {α : Type u} → [inst : AddMonoid α] → AddUnits α → α
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.IsMarkovKernel.snd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) [ProbabilityTheory.IsMarkovKernel κ],
  ProbabilityTheory.IsMarkovKernel κ.snd
-- Mathlib.LinearAlgebra.Dual.Lemmas
/-- The quotient by a subspace is isomorphic to its dual annihilator.  -/
Subspace.quotEquivAnnihilator : {K : Type u_1} →
  {V : Type u_2} →
    [inst : Field K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] →
          [FiniteDimensional K V] → (W : Subspace K V) → (V ⧸ W) ≃ₗ[K] ↥(Submodule.dualAnnihilator W)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_alter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] {k k' : α} {fallback : β} {f : Option β → Option β},
  m.WF → (m.alter k f).getD k' fallback = if (k == k') = true then (f m[k]?).getD fallback else m.getD k' fallback
-- Init.Data.String.PosRaw
String.Pos.Raw.increaseBy_charUtf8Size : ∀ {p : String.Pos.Raw} {c : Char}, p.increaseBy c.utf8Size = p + c
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_mul_mul : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10}
  {m : MeasurableSpace β} [inst : Mul β] [MeasurableMul₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k l : ι), i ≠ k → i ≠ l → j ≠ k → j ≠ l → ProbabilityTheory.IndepFun (f i * f j) (f k * f l) μ
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.associator.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X Y Z : CategoryTheory.Center C),
  X.associator Y Z =
    CategoryTheory.Center.isoMk
      { f := (CategoryTheory.MonoidalCategoryStruct.associator X.fst Y.fst Z.fst).hom, comm := ⋯ }
-- Mathlib.MeasureTheory.OuterMeasure.AE
Set.indicator_ae_eq_zero : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {M : Type u_4} [inst_2 : Zero M] {f : α → M} {s : Set α},
  s.indicator f =ᵐ[μ] 0 ↔ μ (s ∩ Function.support f) = 0
-- Lean.Elab.DeclNameGen
_private.Lean.Elab.DeclNameGen.0.Lean.Elab.Command.NameGen.mkBaseNameCore.visit'.match_1.eq_2 : ∀ (motive : Lean.Name → Sort u_1) (x : Lean.Name) (h_1 : (pre : Lean.Name) → (str : String) → motive (pre.str str))
  (h_2 : (x : Lean.Name) → motive x),
  (∀ (pre : Lean.Name) (str : String), x = pre.str str → False) →
    (match x with
      | pre.str str => h_1 pre str
      | x => h_2 x) =
      h_2 x
-- Init.Data.SInt.Bitwise
Int64.toBitVec_shiftRight : ∀ (a b : Int64), (a >>> b).toBitVec = a.toBitVec.sshiftRight' (b.toBitVec.smod 64)
-- Mathlib.Analysis.Normed.Group.Continuity
tendsto_norm_inv_mul_self : ∀ {E : Type u_4} [inst : SeminormedGroup E] (x : E), Filter.Tendsto (fun a => ‖a⁻¹ * x‖) (nhds x) (nhds 0)
-- Mathlib.CategoryTheory.Sites.InducedTopology
CategoryTheory.Functor.mem_restrictedTopology_of_functorPushforward_mem : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {K : CategoryTheory.GrothendieckTopology D} {X : C} {S : CategoryTheory.Sieve X},
  CategoryTheory.Sieve.functorPushforward F S ∈ K (F.obj X) → S ∈ (F.restrictedTopology K) X
-- Std.Internal.Do.ExceptPost
/-- Pretty-print `EPost.Nil` as `EPost⟨⟩`.  -/
Std.Internal.Do.unexpandEPostNil : Lean.PrettyPrinter.Unexpander
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerve_hom_app : ∀ {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)
  (X : SimplexCategoryᵒᵖ), (U.cechIsoCechNerve hT).hom.app X = (U.cechIsoCechNerveApp hT X).hom
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabDelayedAssignedMVar : Lean.PrettyPrinter.Delaborator.Delab
-- Init.Data.Int.Order
Int.sub_pos : ∀ {a b : ℤ}, 0 < a - b ↔ b < a
-- Init.GrindInstances.Ring.UInt
UInt64.intCast_ofNat : ∀ (x : ℕ), ↑(OfNat.ofNat x) = OfNat.ofNat x
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instInhabited : {α : Type u_1} → {β : Type u_2} → {l : Filter α} → [Inhabited β] → Inhabited (l.Germ β)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get!_diff_of_not_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} [inst_2 : Inhabited β], k ∉ m₂ → (m₁ \ m₂).get! k = m₁.get! k
-- Mathlib.CategoryTheory.Monoidal.End
/-- If `m ⊗ n ≅ 𝟙_M`, then `F.obj m` is a left inverse of `F.obj n`.  -/
CategoryTheory.unitOfTensorIsoUnit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {M : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} M] →
        [inst_2 : CategoryTheory.MonoidalCategory M] →
          (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) →
            (m n : M) →
              (CategoryTheory.MonoidalCategoryStruct.tensorObj m n ≅
                  CategoryTheory.MonoidalCategoryStruct.tensorUnit M) →
                [F.Monoidal] → (F.obj m).comp (F.obj n) ≅ CategoryTheory.Functor.id C
-- Mathlib.RingTheory.Localization.Submodule
IsLocalization.coeSubmodule_injective : ∀ {R : Type u_3} [inst : CommRing R] {M : Submonoid R} (S : Type u_4) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [IsLocalization M S], M ≤ nonZeroDivisors R → Function.Injective (IsLocalization.coeSubmodule S)
-- Mathlib.Condensed.TopCatAdjunction
/-- The adjunction `condensedSetToTopCat ⊣ topCatToCondensedSet` restricted to compactly generated
spaces.
 -/
CondensedSet.compactlyGeneratedAdjunction : CondensedSet.condensedSetToCompactlyGenerated ⊣ CondensedSet.compactlyGeneratedToCondensedSet
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
CategoryTheory.Functor.instIsWellOrderContinuousCompFunctorEquivalence : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : PartialOrder J]
  (F : CategoryTheory.Functor J C) {J' : Type w'} [inst_2 : PartialOrder J'] (e : J' ≃o J) [F.IsWellOrderContinuous],
  (e.equivalence.functor.comp F).IsWellOrderContinuous
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_insertMany_emptyWithCapacity_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {l : List ((a : α) × β a)}
  {k : α},
  (List.map Sigma.fst l).contains k = false →
    (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).get? k = none
-- Init.Data.List.MinMaxIdx
List.minIdxOn_eq_zero_iff : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {xs : List α}
  {f : α → β} (h : xs ≠ []), List.minIdxOn f xs h = 0 ↔ ∀ x ∈ xs, f (xs.head h) ≤ f x
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tsum_singleton : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (b : β) (f : β → α),
  ∑' (x : ↑{b}), f ↑x = f b
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.smulCommClass' : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {R₁ : Type u_5} {R₂ : Type u_6} {s : ι → Type u_7}
  [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] [inst_3 : Monoid R₁]
  [inst_4 : DistribMulAction R₁ R] [inst_5 : SMulCommClass R₁ R R] [inst_6 : Monoid R₂] [inst_7 : DistribMulAction R₂ R]
  [inst_8 : SMulCommClass R₂ R R] [SMulCommClass R₁ R₂ R], SMulCommClass R₁ R₂ (PiTensorProduct R fun i => s i)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner
MeasureTheory.AEStronglyMeasurable.re : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → 𝕜},
  MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable (fun x => RCLike.re (f x)) μ
-- Mathlib.Topology.Algebra.UniformConvergence
UniformOnFun.toFun_mul : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : Mul β] (f g : UniformOnFun α β 𝔖),
  (UniformOnFun.toFun 𝔖) (f * g) = (UniformOnFun.toFun 𝔖) f * (UniformOnFun.toFun 𝔖) g
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.blockTriangular_blockDiagonal' : ∀ {α : Type u_1} {m' : α → Type u_6} {R : Type v} [inst : Preorder α] [inst_1 : Zero R] [inst_2 : DecidableEq α]
  (d : (i : α) → Matrix (m' i) (m' i) R), (Matrix.blockDiagonal' d).BlockTriangular Sigma.fst
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
CategoryTheory.JointlyReflectIsomorphisms.mono : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] {I : Type u_2} {D : I → Type u_3}
  [inst_1 : (i : I) → CategoryTheory.Category.{u_5, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)},
  CategoryTheory.JointlyReflectIsomorphisms F →
    ∀ {X Y : C} (f : X ⟶ Y) [hf : ∀ (i : I), CategoryTheory.Mono ((F i).map f)]
      [∀ (i : I), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f f) (F i)]
      [CategoryTheory.Limits.HasPullback f f], CategoryTheory.Mono f
-- Init.Data.Int.DivMod.Lemmas
Int.fdiv_eq_ediv : ∀ {a b : ℤ}, a.fdiv b = a / b - if 0 ≤ b ∨ b ∣ a then 0 else 1
-- Init.Data.Int.Order
Int.ne_of_gt : ∀ {a b : ℤ}, b < a → a ≠ b
-- Mathlib.Analysis.Meromorphic.Divisor
/-- Simplifier lemma: on `U`, the divisor of a function `f` that is meromorphic on `U` evaluates to
`order.untop₀`.
 -/
MeromorphicOn.divisor_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {z : 𝕜} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E},
  MeromorphicOn f U → z ∈ U → (MeromorphicOn.divisor f U) z = (meromorphicOrderAt f z).untop₀
-- Mathlib.Algebra.Star.MonoidHom
/-- The inverse of a star monoid isomorphism is a star monoid isomorphism.  -/
StarMulEquiv.symm : {A : Type u_2} →
  {B : Type u_3} → [inst : Mul A] → [inst_1 : Mul B] → [inst_2 : Star A] → [inst_3 : Star B] → (A ≃⋆* B) → B ≃⋆* A
-- Mathlib.Data.Setoid.Basic
Setoid.bot_def : ∀ {α : Type u_1}, ⇑⊥ = fun x1 x2 => x1 = x2
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolInformation.kind : Lean.Lsp.SymbolInformation → Lean.Lsp.SymbolKind
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.ofLinear_apply : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂}
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (f : M →ₛₗ[σ₁₂] M₂)
  (g : M₂ →ₛₗ[σ₂₁] M) {h₁ : f ∘ₛₗ g = LinearMap.id} {h₂ : g ∘ₛₗ f = LinearMap.id} (x : M),
  (LinearEquiv.ofLinear f g h₁ h₂) x = f x
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.vanishingIdeal_closure : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (t : Set (ProjectiveSpectrum 𝒜)),
  ProjectiveSpectrum.vanishingIdeal (closure t) = ProjectiveSpectrum.vanishingIdeal t
-- Init.Data.UInt.Lemmas
UInt8.toFin_ofNatClamp_of_le : ∀ {n : ℕ}, UInt8.size ≤ n → (UInt8.ofNatClamp n).toFin = ⟨UInt8.size - 1, UInt8.toFin_ofNatClamp_of_le._proof_1⟩
-- Lean.Data.Lsp.Internal
Lean.Lsp.RefIdent.instFromJsonRefIdentJsonRepr.fromJson : Lean.Json → Except String Lean.Lsp.RefIdent.RefIdentJsonRepr
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instStar : {R : Type u_1} → {A : Type u_2} → [Star R] → [Star A] → Star (Unitization R A)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_eq_getD : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : LawfulBEq α]
  {a : α} {fallback : β}, Std.ExtDHashMap.Const.getD m a fallback = m.getD a fallback
-- Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
integrableOn_Ioi_exp_neg_mul_sq_iff : ∀ {b : ℝ}, MeasureTheory.IntegrableOn (fun x => Real.exp (-b * x ^ 2)) (Set.Ioi 0) MeasureTheory.volume ↔ 0 < b
-- Mathlib.Order.Category.BoolAlg
HeytingHom.mk.congr_simp : ∀ {α : Type u_6} {β : Type u_7} [inst : HeytingAlgebra α] [inst_1 : HeytingAlgebra β]
  (toLatticeHom toLatticeHom_1 : LatticeHom α β) (e_toLatticeHom : toLatticeHom = toLatticeHom_1)
  (map_bot' : toLatticeHom.toFun ⊥ = ⊥)
  (map_himp' : ∀ (a b : α), toLatticeHom.toFun (a ⇨ b) = toLatticeHom.toFun a ⇨ toLatticeHom.toFun b),
  { toLatticeHom := toLatticeHom, map_bot' := map_bot', map_himp' := map_himp' } =
    { toLatticeHom := toLatticeHom_1, map_bot' := ⋯, map_himp' := ⋯ }
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.isRamified_mk_iff_isMixed : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K] {φ : K →+* ℂ},
  NumberField.InfinitePlace.IsRamified k (NumberField.InfinitePlace.mk φ) ↔ NumberField.ComplexEmbedding.IsMixed k φ
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsRatStieltjesPoint.ite : ∀ {α : Type u_1} {f g : α → ℚ → ℝ} {a : α} (p : α → Prop) [inst : DecidablePred p],
  (p a → ProbabilityTheory.IsRatStieltjesPoint f a) →
    (¬p a → ProbabilityTheory.IsRatStieltjesPoint g a) →
      ProbabilityTheory.IsRatStieltjesPoint (fun a => if p a then f a else g a) a
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_left' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Z)
  (g : Y ⟶ Z) [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f],
  CategoryTheory.Limits.HasLimit
    (CategoryTheory.Limits.cospan
      (((CategoryTheory.Limits.cospan f g).comp AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace).map
        CategoryTheory.Limits.WalkingCospan.Hom.inl)
      (((CategoryTheory.Limits.cospan f g).comp AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace).map
        CategoryTheory.Limits.WalkingCospan.Hom.inr))
-- Mathlib.RingTheory.Idempotents
AlgEquiv.prodQuotientOfIsIdempotentElem_apply_snd : ∀ (R : Type u_1) [inst : CommRing R] {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S] {e f : S}
  (he : IsIdempotentElem e) (hf : IsIdempotentElem f) (hef₁ : e + f = 1) (hef₂ : e * f = 0) (a : S),
  ((AlgEquiv.prodQuotientOfIsIdempotentElem R he hf hef₁ hef₂) a).2 = (Ideal.Quotient.mk (Ideal.span {f})) a
-- Mathlib.Algebra.Group.Defs
ZPow.ofPow : {M : Type u_2} → [Pow M ℤ] → ZPow M
-- Mathlib.Tactic.CrossRefAttribute
/-- Returns the array of `Tag`s in the environment, sorted alphabetically by tag.  -/
_private.Mathlib.Tactic.CrossRefAttribute.0.Lean.Environment.getSortedCrossRefs : Lean.Environment → Array Mathlib.CrossRef.Tag
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.instBEqOrigin : BEq Lean.Meta.Origin
-- Mathlib.Data.Fin.Tuple.Take
Fin.take_eq_init : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_2} (v : (i : Fin (n + 1)) → α i), Fin.take n ⋯ v = Fin.init v
-- Mathlib.RingTheory.HahnSeries.Lex
/-- `HahnSeries.embDomain` as an `OrderAddMonoidHom`.  -/
HahnSeries.embDomainOrderAddMonoidHom : {Γ : Type u_1} →
  {R : Type u_2} →
    [inst : LinearOrder Γ] →
      [inst_1 : PartialOrder R] →
        {Γ' : Type u_3} →
          [inst_2 : LinearOrder Γ'] → Γ ↪o Γ' → [inst_3 : AddMonoid R] → Lex (HahnSeries Γ R) →+o Lex (HahnSeries Γ' R)
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
QuadraticMap.IsometryEquiv.mk.inj : ∀ {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} {inst : CommSemiring R} {inst_1 : AddCommMonoid M₁}
  {inst_2 : AddCommMonoid M₂} {inst_3 : AddCommMonoid N} {inst_4 : Module R M₁} {inst_5 : Module R M₂}
  {inst_6 : Module R N} {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} {toLinearEquiv : M₁ ≃ₗ[R] M₂}
  {map_app' : ∀ (m : M₁), Q₂ ((↑toLinearEquiv).toFun m) = Q₁ m} {toLinearEquiv_1 : M₁ ≃ₗ[R] M₂}
  {map_app'_1 : ∀ (m : M₁), Q₂ ((↑toLinearEquiv_1).toFun m) = Q₁ m},
  { toLinearEquiv := toLinearEquiv, map_app' := map_app' } =
      { toLinearEquiv := toLinearEquiv_1, map_app' := map_app'_1 } →
    toLinearEquiv = toLinearEquiv_1
-- Init.Data.UInt.Bitwise
instLawfulCommIdentityUSizeHAndNegOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 &&& x2) (-1)
-- Init.Data.UInt.Lemmas
BitVec.ofNatLT_uInt64ToNat : ∀ (n : UInt64), n.toNat#'⋯ = n.toBitVec
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.smul_mk'_one : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (x : R) (m : ↥M),
  x • IsLocalization.mk' S 1 m = IsLocalization.mk' S x m
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Grothendieck.ιCompMap.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C CategoryTheory.Cat}
  (α : F ⟶ F') (c : C),
  CategoryTheory.Grothendieck.ιCompMap α c =
    CategoryTheory.NatIso.ofComponents
      (fun X =>
        CategoryTheory.Iso.refl (((CategoryTheory.Grothendieck.ι F c).comp (CategoryTheory.Grothendieck.map α)).obj X))
      ⋯
-- Mathlib.Tactic.IntervalCases
Mathlib.Tactic.IntervalCases.Bound.le.inj : ∀ {n n_1 : ℤ}, Mathlib.Tactic.IntervalCases.Bound.le n = Mathlib.Tactic.IntervalCases.Bound.le n_1 → n = n_1
-- Mathlib.MeasureTheory.VectorMeasure.WithDensity
MeasureTheory.withDensityᵥ_smul' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {𝕜 : Type u_3} [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 E]
  [SMulCommClass ℝ 𝕜 E] (f : α → E) (r : 𝕜), (μ.withDensityᵥ fun x => r • f x) = r • μ.withDensityᵥ f
-- Mathlib.Combinatorics.Matroid.Map
Matroid.restrictSubtype_dual : ∀ {α : Type u_1} {M : Matroid α}, (M.restrictSubtype M.E)✶ = M✶.restrictSubtype M.E
-- Mathlib.Combinatorics.Enumerative.Composition
List.splitWrtCompositionAux.eq_def : ∀ {α : Type u_1} (x : List α) (x_1 : List ℕ),
  x.splitWrtCompositionAux x_1 =
    match x, x_1 with
    | x, [] => []
    | l, n :: ns =>
      match List.splitAt n l with
      | (l₁, l₂) => l₁ :: l₂.splitWrtCompositionAux ns
-- Mathlib.Dynamics.Ergodic.Conservative
/-- If `f` is a conservative self-map and `s` is a null measurable set of nonzero measure,
then there exists a point `x ∈ s` that returns to `s` under a non-zero iteration of `f`.  -/
MeasureTheory.Conservative.exists_mem_iterate_mem : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → α} {s : Set α} {μ : MeasureTheory.Measure α},
  MeasureTheory.Conservative f μ → MeasureTheory.NullMeasurableSet s μ → μ s ≠ 0 → ∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[m] x ∈ s
-- Mathlib.Logic.Function.Basic
Function.not_bijective : Function.Bijective Not
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instIsValuativeTopology : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀),
  IsValuativeTopology (WithVal v)
-- Mathlib.CategoryTheory.ObjectProperty.Small
_private.Mathlib.CategoryTheory.ObjectProperty.Small.0.CategoryTheory.ObjectProperty.instSmallMax.match_1.eq_2 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] {P Q : CategoryTheory.ObjectProperty C}
  (motive : Subtype P ⊕ Subtype Q → Sort u_2) (x : Subtype Q) (h_1 : (x : Subtype P) → motive (Sum.inl x))
  (h_2 : (x : Subtype Q) → motive (Sum.inr x)),
  (match Sum.inr x with
    | Sum.inl x => h_1 x
    | Sum.inr x => h_2 x) =
    h_2 x
-- Mathlib.LinearAlgebra.Matrix.ToLin
Module.Basis.smulTower.congr_simp : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid A]
  [inst_3 : Module R S] [inst_4 : Module S A] [inst_5 : Module R A] [inst_6 : IsScalarTower R S A] {ι : Type u_5}
  {ι' : Type u_6} (b b_1 : Module.Basis ι R S),
  b = b_1 → ∀ (c c_1 : Module.Basis ι' S A), c = c_1 → b.smulTower c = b_1.smulTower c_1
-- Mathlib.Data.Set.Function
Set.mapsTo_of_subsingleton : ∀ {α : Type u_1} [Subsingleton α] (f : α → α) (s : Set α), Set.MapsTo f s s
-- Mathlib.Analysis.Calculus.FDeriv.Prod
differentiableAt_finCons : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {n : ℕ} {F' : Fin n.succ → Type u_6}
  [inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_4 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ},
  DifferentiableAt 𝕜 (fun x => Fin.cons (φ x) (φs x)) x ↔ DifferentiableAt 𝕜 φ x ∧ DifferentiableAt 𝕜 φs x
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.add_le_aleph0 : ∀ {c₁ c₂ : Cardinal.{u_1}}, c₁ + c₂ ≤ Cardinal.aleph0 ↔ c₁ ≤ Cardinal.aleph0 ∧ c₂ ≤ Cardinal.aleph0