mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.List.Basic
Function.RightInverse.list_map : ∀ {α : Type u} {β : Type v} {f : α → β} {g : β → α},
  Function.RightInverse f g → Function.RightInverse (List.map f) (List.map g)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.drop_length : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n : ℕ), (p.drop n).length = p.length - n
-- Mathlib.Analysis.Meromorphic.Divisor
/-- Special case of `Function.locallyFinsuppWithin.finiteSupport` that frequently shows in complex
analysis: Divisors on spheres have finite support.
 -/
divisor_sphere_support_finite : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [ProperSpace 𝕜] {f : 𝕜 → E} {R : ℝ} {c : 𝕜},
  (MeromorphicOn.divisor f (Metric.sphere c R)).support.Finite
-- Mathlib.Analysis.Convex.Extreme
/-- `x` is an extreme point to `A` iff `{x}` is an extreme set of `A`.  -/
isExtreme_singleton : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {A : Set E} {x : E}, IsExtreme 𝕜 A {x} ↔ x ∈ Set.extremePoints 𝕜 A
-- Mathlib.RingTheory.FreeCommRing
FreeRing.instCommRing : (α : Type u) → [Subsingleton α] → CommRing (FreeRing α)
-- Lean.Data.Options
Lean.OptionDecl.deprecation? : Lean.OptionDecl → Option Lean.OptionDeprecation
-- Mathlib.Algebra.Ring.AddAut
/-- Right multiplication by a unit of a semiring as an additive automorphism.  -/
AddAut.mulRight : {R : Type u_1} → [inst : Semiring R] → Rˣ → AddAut R
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.foldr_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} {δ : Type w} [Std.TransCmp cmp] {f : α → δ → δ}
  {init : δ}, t₁.WF → t₂.WF → t₁.Equiv t₂ → Std.TreeSet.Raw.foldr f init t₁ = Std.TreeSet.Raw.foldr f init t₂
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.Indep.inter_right : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.Indep I → ∀ (X : Set α), M.Indep (I ∩ X)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inr_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ],
  (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)).comp ↑(CochainComplex.mappingCone.fst φ)
      ⋯ =
    0
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.mem_closedEBall'`. -/
EMetric.mem_closedBall' : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {ε : ENNReal}, y ∈ Metric.closedEBall x ε ↔ edist x y ≤ ε
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_inv_app_comp_snd_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X : C} (g : Z ⟶ X)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g] (T : CategoryTheory.Over X) {Z_1 : C} (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left ((CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback g).inv.app T))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd T.hom g) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd T.hom g) h
-- Mathlib.Logic.Function.Defs
Function.const_prod : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} (p : α × β),
  Function.const ι p = Function.prod (Function.const ι p.1) (Function.const ι p.2)
-- Init.Grind.FieldNormNum
Lean.Grind.Field.NormNum.ofRat_add : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] [Lean.Grind.IsCharP α 0] (a b : ℚ),
  Lean.Grind.Field.NormNum.ofRat (a + b) = Lean.Grind.Field.NormNum.ofRat a + Lean.Grind.Field.NormNum.ofRat b
-- Lean.ExtraModUses
_private.Lean.ExtraModUses.0.Lean.extraModUses : Lean.SimplePersistentEnvExtension Lean.ExtraModUse (Lean.PHashSet Lean.ExtraModUse)
-- Init.Data.ByteArray.Basic
ByteArray.append_eq_fastAppend : ByteArray.append = ByteArray.fastAppend
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.take.eq_1 : ∀ (p : DyckWord) (i : ℕ) (hi : List.count DyckStep.U (List.take i ↑p) = List.count DyckStep.D (List.take i ↑p)),
  p.take i hi = { toList := List.take i ↑p, count_U_eq_count_D := hi, count_D_le_count_U := ⋯ }
-- Mathlib.Tactic.NormNum.Basic
/-- The result of subtracting two `norm_num` results.  -/
Mathlib.Meta.NormNum.Result.sub : {u : Lean.Level} →
  {α : Q(Type u)} →
    {a b : Q(«$α»)} →
      Mathlib.Meta.NormNum.Result q(«$a») →
        Mathlib.Meta.NormNum.Result q(«$b») →
          (inst : autoParam Q(Ring «$α») Mathlib.Meta.NormNum.Result.sub._auto_1) →
            Lean.MetaM (Mathlib.Meta.NormNum.Result q(«$a» - «$b»))
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.getElimInfo : Lean.Name → optParam (Option Lean.Name) none → Lean.MetaM Lean.Meta.ElimInfo
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.ExtraTheorem.fvar.inj : ∀ {fvarId fvarId_1 : Lean.FVarId},
  Lean.Elab.Tactic.Grind.ExtraTheorem.fvar fvarId = Lean.Elab.Tactic.Grind.ExtraTheorem.fvar fvarId_1 →
    fvarId = fvarId_1
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.mem_toNonUnitalSubsemiring : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  {S : NonUnitalSubalgebra R A} {x : A}, x ∈ S.toNonUnitalSubsemiring ↔ x ∈ S
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
SubAddAction.ofStabilizer.isMultiplyPretransitive_iff_of_addConj : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {n : ℕ} {a b : α} {g : G},
  b = g +ᵥ a →
    (AddAction.IsMultiplyPretransitive (↥(AddAction.stabilizer G a)) (↥(SubAddAction.ofStabilizer G a)) n ↔
      AddAction.IsMultiplyPretransitive (↥(AddAction.stabilizer G b)) (↥(SubAddAction.ofStabilizer G b)) n)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.restrict_lt_one_iff : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
  {x : R}, v.restrict x < 1 ↔ v x < 1
-- Mathlib.NumberTheory.MulChar.Basic
/-- The square of a quadratic character is the trivial character.  -/
MulChar.IsQuadratic.sq_eq_one : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommRing R'] {χ : MulChar R R'},
  χ.IsQuadratic → χ ^ 2 = 1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.isEmpty_toList : ∀ {α : Type u} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  (Std.DTreeMap.Internal.Impl.Const.toList t).isEmpty = t.isEmpty
-- Mathlib.Order.SetNotation
Set.mem_sInter : ∀ {α : Type u} {x : α} {S : Set (Set α)}, x ∈ ⋂₀ S ↔ ∀ t ∈ S, x ∈ t
-- Mathlib.Topology.Category.Locale
/-- The forgetful functor from `Top` to `Locale` which forgets that the space has "enough points".
 -/
topToLocale : CategoryTheory.Functor TopCat Locale
-- Init.Data.Range.Polymorphic.PRange
Std.Roo.HasRcoIntersection.mk : {α : Type w} → (Std.Roo α → Std.Rco α → Std.Rco α) → Std.Roo.HasRcoIntersection α
-- Mathlib.ModelTheory.Syntax
/-- The biimplication between two bounded formulas.  -/
FirstOrder.«term_⇔_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.Coprime.Lemmas
IsRelPrime.prod_left : ∀ {α : Type u_2} {I : Type u_1} [inst : CommMonoid α] [DecompositionMonoid α] {x : α} {s : I → α} {t : Finset I},
  (∀ i ∈ t, IsRelPrime (s i) x) → IsRelPrime (∏ i ∈ t, s i) x
-- Mathlib.Analysis.CStarAlgebra.Unitary.Span
/-- A unital C⋆-algebra is spanned by its unitary elements.  -/
CStarAlgebra.span_unitary : ∀ (A : Type u_1) [inst : CStarAlgebra A], Submodule.span ℂ ↑(unitary A) = ⊤
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.ofCoeff.sizeOf_spec : ∀ {R : Type u_8} {M : Type u_9} [inst : Semiring R] [inst_1 : SizeOf R] [inst_2 : SizeOf M] (coeff : M →₀ R),
  sizeOf (AddMonoidAlgebra.ofCoeff coeff) = 1 + sizeOf coeff
-- Mathlib.Algebra.Category.MonCat.Limits
MonCat.forget_createsLimitsOfShape.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J],
  MonCat.forget_createsLimitsOfShape = { CreatesLimit := fun {K} => inferInstance }
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.collectPatterns? : Lean.Expr →
  Array Lean.Expr →
    Array Lean.Expr →
      Lean.Meta.Grind.SymbolPriorities → ℕ → Bool → Lean.MetaM (Option (List Lean.Expr × List Lean.HeadIndex))
-- Init.System.ST
ST.Out.mk.inj : ∀ {σ α : Type} {val : α} {state : Void σ} {val_1 : α} {state_1 : Void σ},
  { val := val, state := state } = { val := val_1, state := state_1 } → val = val_1 ∧ state = state_1
-- Mathlib.Logic.Function.FiberPartition
Function.Fiber.map_preimage_eq_image_map : ∀ {Y : Type u_2} {Z : Type u_3} {W : Type u_4} (f : Y → Z) (g : Z → W) (a : Function.Fiber (g ∘ f)),
  g (f (Function.Fiber.preimage (g ∘ f) a)) = Function.Fiber.image (g ∘ f) a
-- Lean.Parser.Attr
Lean.Parser.Attr.macro.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Data.Vector.Defs
/-- A nil vector maps to a nil list.  -/
List.Vector.toList_nil : ∀ {α : Type u_1}, List.Vector.nil.toList = []
-- Mathlib.RingTheory.Ideal.Maps
Ideal.ker_le_comap : ∀ {R : Type u_1} {S : Type u_2} {F : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S]
  [rc : RingHomClass F R S] {K : Ideal S} (f : F), RingHom.ker f ≤ Ideal.comap f K
-- Mathlib.GroupTheory.Submonoid.Inverses
Submonoid.leftInvEquiv_symm_eq_inv : ∀ {M : Type u_1} [inst : CommGroup M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) (x : ↥S),
  ↑((S.leftInvEquiv hS).symm x) = (↑x)⁻¹
-- Init.Data.Range.Polymorphic.IntLemmas
/-- Induction principle for proving properties of `Int`-based ranges of the form `a...=b` by
varying the lower bound.

In the `base` case, one proves that for any `a : Int` and `b : Int` with
`b < a`, the statement holds for the empty range `a...=b`.

In the `step` case, one proves that for any `a : Int` and `b : Int`, the
statement holds for nonempty ranges `a...b` if it holds for the smaller range
`(a + 1)...=b`.

The following is an example reproving `length_toList_rcc`.

```
example (a b : Int) : (a...=b).toList.length = (b + 1 - a).toNat := by
  induction a, b using Int.induct_rcc_left
  case base =>
    simp only [Int.toList_rcc_eq_nil, List.length_nil, Int.zero_eq_toNat_sub_iff, *]; omega
  case step =>
    simp only [Int.toList_rcc_eq_cons, List.length_cons, *]; omega
``` -/
Int.induct_rcc_left : ∀ (motive : ℤ → ℤ → Prop),
  (∀ (a b : ℤ), b < a → motive a b) → (∀ (a b : ℤ), a ≤ b → motive (a + 1) b → motive a b) → ∀ (a b : ℤ), motive a b
-- Init.Data.UInt.Lemmas
UInt8.neg_zero : -0 = 0
-- Batteries.Recycling.RBTree.Basic
/-- `O(1)` amortized, `O(log n)` worst case: Get the next element from the stream.  -/
RBTree.RBNode.Stream.next? : {α : Type u_1} → RBTree.RBNode.Stream α → Option (α × RBTree.RBNode.Stream α)
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.span_eq_toSubmodule : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  (s : NonUnitalSubalgebra R A), Submodule.span R ↑s = s.toSubmodule
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.orElim'.sizeOf_spec : ∀ (p₁ : Mathlib.Tactic.ITauto.Proof) (x : Lean.Name) (p₂ p₃ : Mathlib.Tactic.ITauto.Proof),
  sizeOf (p₁.orElim' x p₂ p₃) = 1 + sizeOf p₁ + sizeOf x + sizeOf p₂ + sizeOf p₃
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
/-- If an alternating map in finitely many variables on a normed space satisfies the inequality
`‖f m‖ ≤ C * ∏ i, ‖m i‖` on a shell `ε i / ‖c i‖ < ‖m i‖ < ε i` for some positive numbers `ε i`
and elements `c i : 𝕜`, `1 < ‖c i‖`, then it satisfies this inequality for all `m`.  -/
AlternatingMap.bound_of_shell : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : Fintype ι] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : SeminormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] (f : F [⋀^ι]→ₗ[𝕜] E) {ε : ι → ℝ} {C : ℝ} {c : ι → 𝕜},
  (∀ (i : ι), 0 < ε i) →
    (∀ (i : ι), 1 < ‖c i‖) →
      (∀ (m : ι → F), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i, ‖m i‖) →
        ∀ (m : ι → F), ‖f m‖ ≤ C * ∏ i, ‖m i‖
-- Mathlib.Order.WellQuasiOrder
OrderHom.wellQuasiOrderedLE_of_wellQuasiOrderedLE_of_surjective : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [WellQuasiOrderedLE α] (f : α →o β),
  Function.Surjective ⇑f → WellQuasiOrderedLE β
-- Mathlib.Data.Set.Finite.Basic
Set.Infinite.nonempty : ∀ {α : Type u} {s : Set α}, s.Infinite → s.Nonempty
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.unop : C ⥤ D` creates finite colimits, then `F : Cᵒᵖ ⥤ Dᵒᵖ` creates finite limits.  -/
CategoryTheory.Limits.createsFiniteLimitsOfUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) →
          [CategoryTheory.Limits.CreatesFiniteColimits F.unop] → CategoryTheory.Limits.CreatesFiniteLimits F
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.toSentence.eq_2 : FirstOrder.Field.FieldAxiom.zeroAdd.toSentence =
  ((0 + (FirstOrder.Language.var ∘ Sum.inr) 0).bdEqual ((FirstOrder.Language.var ∘ Sum.inr) 0)).all
-- Mathlib.Data.Nat.Choose.Multinomial
Multiset.countPerms_zero : ∀ {α : Type u_1} [inst : DecidableEq α], Multiset.countPerms 0 = 1
-- Mathlib.FieldTheory.Isaacs
/-- **Alias** of `Field.nonempty_algHom_of_exists_root`. -/
Field.nonempty_algHom_of_exist_roots : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] [alg : Algebra.IsAlgebraic F E],
  (∀ (x : E), ∃ y, (Polynomial.aeval y) (minpoly F x) = 0) → Nonempty (E →ₐ[F] K)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- The braiding isomorphism as a natural isomorphism of bifunctors `C ⥤ C ⥤ C`.  -/
CategoryTheory.BraidedCategory.curriedBraidingNatIso : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] →
        CategoryTheory.MonoidalCategory.curriedTensor C ≅ (CategoryTheory.MonoidalCategory.curriedTensor C).flip
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.martingale_of_setIntegral_eq_succ : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {𝒢 : MeasureTheory.Filtration ℕ m0} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ]
  {f : ℕ → Ω → E},
  MeasureTheory.StronglyAdapted 𝒢 f →
    (∀ (i : ℕ), MeasureTheory.Integrable (f i) μ) →
      (∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ = ∫ (ω : Ω) in s, f (i + 1) ω ∂μ) →
        MeasureTheory.Martingale f 𝒢 μ
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepSets.precomp : ∀ {Ω : Type u_1} {ι : Type u_2} {π : ι → Set (Set Ω)} {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  {ι' : Type u_6} {g : ι' → ι},
  Function.Injective g → ProbabilityTheory.iIndepSets π μ → ProbabilityTheory.iIndepSets (π ∘ g) μ
-- Mathlib.Data.Finset.Finsupp
Finset.mem_finsupp_iff : ∀ {ι : Type u_1} {α : Type u_2} [inst : Zero α] {s : Finset ι} {f : ι →₀ α} {t : ι → Finset α},
  f ∈ s.finsupp t ↔ f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i
-- Init.Data.List.Basic
List.all_cons : ∀ {α : Type u_1} {a : α} {l : List α} {f : α → Bool}, (a :: l).all f = (f a && l.all f)
-- Mathlib.Analysis.Seminorm
/-- A seminorm is continuous at `0` if `p.closedBall 0 r ∈ 𝓝 0` for *all* `r > 0`.
Over a `NontriviallyNormedField` it is actually enough to check that this is true
for *some* `r`, see `Seminorm.continuousAt_zero'`.  -/
Seminorm.continuousAt_zero_of_forall' : ∀ {𝕝 : Type u_6} {E : Type u_7} [inst : SeminormedRing 𝕝] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕝 E]
  [inst_3 : TopologicalSpace E] {p : Seminorm 𝕝 E}, (∀ r > 0, p.closedBall 0 r ∈ nhds 0) → ContinuousAt (⇑p) 0
-- Mathlib.Data.Sigma.Basic
Function.Surjective.eq_1 : ∀ {α : Sort u_1} {β : Sort u_2} (f : α → β), Function.Surjective f = ∀ (b : β), ∃ a, f a = b
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.dilatransvection.congr_simp : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  {f f_1 : Module.Dual R V} (e_f : f = f_1) {v v_1 : V} (e_v : v = v_1) (h : IsUnit (1 + f v)),
  LinearEquiv.dilatransvection h = LinearEquiv.dilatransvection ⋯
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.ext : ∀ {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₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] {f g : E →ₛₗᵢ[σ₁₂] E₂}, (∀ (x : E), f x = g x) → f = g
-- Mathlib.Analysis.Distribution.Distribution
Distribution.instLineDerivAddTopENat : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_2}
  [inst_2 : AddCommGroup F] [inst_3 : Module ℝ F] [inst_4 : TopologicalSpace F] [inst_5 : IsTopologicalAddGroup F]
  [inst_6 : ContinuousSMul ℝ F], LineDerivAdd E (Distribution Ω F ⊤) (Distribution Ω F ⊤)
-- Mathlib.Control.ULiftable
instULiftableWriterTULift : {s : Type u₀} →
  {m : Type u₀ → Type u_5} →
    {m' : Type (max u₀ u_6) → Type u_7} → [ULiftable m m'] → ULiftable (WriterT s m) (WriterT (ULift.{u_6, u₀} s) m')
-- Mathlib.RingTheory.LocalRing.ResidueField.Fiber
Ideal.Fiber.exists_smul_eq_one_tmul : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : p.IsPrime] (x : p.Fiber S), ∃ r ∉ p, ∃ s, r • x = 1 ⊗ₜ[R] s
-- Mathlib.Analysis.Convex.Visible
IsVisible.mono : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : AddCommGroup V]
  [inst_3 : Module 𝕜 V] [inst_4 : AddTorsor V P] {s t : Set P} {x y : P}, s ⊆ t → IsVisible 𝕜 t x y → IsVisible 𝕜 s x y
-- Mathlib.Data.Set.Countable
Set.Countable.biUnion_iff : ∀ {α : Type u} {β : Type v} {s : Set α} {t : (a : α) → a ∈ s → Set β},
  s.Countable → ((⋃ a, ⋃ (h : a ∈ s), t a h).Countable ↔ ∀ (a : α) (ha : a ∈ s), (t a ha).Countable)
-- Mathlib.GroupTheory.OreLocalization.Basic
_private.Mathlib.GroupTheory.OreLocalization.Basic.0.AddOreLocalization.vadd' : {R : Type u_1} →
  [inst : AddMonoid R] →
    {S : AddSubmonoid R} →
      [inst_1 : AddOreLocalization.AddOreSet S] →
        {X : Type u_2} → [inst_2 : AddAction R X] → R → ↥S → X → ↥S → AddOreLocalization S X
-- Mathlib.CategoryTheory.ObjectProperty.Equivalence
CategoryTheory.ObjectProperty.topEquivalence_functor : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C], (CategoryTheory.ObjectProperty.topEquivalence C).functor = ⊤.ι
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.indepSets_piiUnionInter_of_disjoint : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ι → Set (Set Ω)}
  {S T : Set ι},
  ProbabilityTheory.iIndepSets s μ →
    Disjoint S T → ProbabilityTheory.IndepSets (piiUnionInter s S) (piiUnionInter s T) μ
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.universally_respectsIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C),
  P.universally.RespectsIso
-- Mathlib.CategoryTheory.Action.Continuous
instConcreteCategoryDiscreteContActionHomSubtypeObjActionIsContinuousContActionIsDiscreteV : (V : Type u_3) →
  [inst : CategoryTheory.Category.{u_2, u_3} V] →
    {FV : V → V → Type u_5} →
      {CV : V → Type u_1} →
        [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory V FV] →
            [inst_3 : CategoryTheory.HasForget₂ V TopCat] →
              (G : Type u_4) →
                [inst_4 : Monoid G] →
                  [inst_5 : TopologicalSpace G] →
                    CategoryTheory.ConcreteCategory (DiscreteContAction V G) fun X Y =>
                      Action.HomSubtype V G X.obj.obj Y.obj.obj
-- Std.Http.Protocol.H1
/-- Returns `true` when `pullBody` can attempt to produce body data immediately.
 -/
Std.Http.Protocol.H1.Machine.canPullBody : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Bool
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sin_add_pi : ∀ (θ : Real.Angle), (θ + ↑Real.pi).sin = -θ.sin
-- Mathlib.Topology.Order.MonotoneContinuity
/-- If a function `f` with a densely ordered codomain is strictly monotone on a left neighborhood of
`a` and the image of this neighborhood under `f` is a left neighborhood of `f a`, then `f` is
continuous at `a` from the left.  -/
StrictMonoOn.continuousWithinAt_left_of_image_mem_nhdsWithin : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : α → β} {s : Set α}
  {a : α},
  StrictMonoOn f s →
    s ∈ nhdsWithin a (Set.Iic a) → f '' s ∈ nhdsWithin (f a) (Set.Iic (f a)) → ContinuousWithinAt f (Set.Iic a) a
-- Mathlib.RingTheory.Localization.Integral
IsFractionRing.integerNormalization_eq_zero_iff : ∀ {A : Type u_3} {K : Type u_4} [inst : CommRing A] [IsDomain A] [inst_2 : Field K] [inst_3 : Algebra A K]
  [inst_4 : IsFractionRing A K] {p : Polynomial K},
  IsLocalization.integerNormalization (nonZeroDivisors A) p = 0 ↔ p = 0
-- Mathlib.Topology.EMetricSpace.Weak
instWeakEMetricSpaceWithBot : {α : Type u} →
  [t : TopologicalSpace α] →
    [inst : LinearOrder α] → [inst_1 : OrderTopology α] → [m : WeakEMetricSpace α] → WeakEMetricSpace (WithBot α)
-- Mathlib.Topology.Sheaves.Sheaf
TopCat.Sheaf.id_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : TopCat) (F : TopCat.Sheaf C X)
  (t : (TopologicalSpace.Opens ↑X)ᵒᵖ),
  (CategoryTheory.CategoryStruct.id F).hom.app t = CategoryTheory.CategoryStruct.id (F.obj.obj t)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List α} {k : α}
  {h : k ∈ Std.ExtTreeMap.unitOfList l cmp}, (Std.ExtTreeMap.unitOfList l cmp)[k] = ()
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- The property of posets in `CardinalDirectedPoset κ` that are
of cardinality `< κ` and have terminal object.  -/
CategoryTheory.CardinalDirectedPoset.hasCardinalLTWithTerminal : (κ : Cardinal.{u}) → [inst : Fact κ.IsRegular] → CategoryTheory.ObjectProperty (CategoryTheory.CardinalDirectedPoset κ)
-- Mathlib.MeasureTheory.Measure.NullMeasurable
/-- A measure is complete if every null set is also measurable.
A null set is a subset of a measurable set with measure `0`.
Since every measure is defined as a special case of an outer measure, we can more simply state
that a set `s` is null if `μ s = 0`.  -/
MeasureTheory.Measure.IsComplete : {α : Type u_2} → {x : MeasurableSpace α} → MeasureTheory.Measure α → Prop
-- Mathlib.CategoryTheory.MorphismProperty.LocalEpi
CategoryTheory.ObjectProperty.instRespectsLocalEpiIsLocal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C},
  P.localEpi.Respects P.isLocal
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.RightHomologyData.canonical_Q : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology],
  (CategoryTheory.ShortComplex.RightHomologyData.canonical S).Q = S.opcycles
-- Mathlib.Analysis.Normed.Affine.AddTorsor
dist_midpoint_left : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] {𝕜 : Type u_5} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 V]
  [inst_5 : Invertible 2] (p₁ p₂ : P), dist (midpoint 𝕜 p₁ p₂) p₁ = ‖2‖⁻¹ * dist p₁ p₂
-- Mathlib.CategoryTheory.Category.Init
/-- Log a message whenever the category theory discharger uses `aesop`.  -/
mathlib.tactic.category.log_aesop : Lean.Option Bool