mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_apply_of_not_and : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {f : R → R} (a : A),
  ¬(p a ∧ ContinuousOn f (spectrum R a)) → cfc f a = 0
-- Lean.Attributes
Lean.AttributeExtensionOLeanEntry : Type
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.mkOfCompact_apply : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : CompactSpace α]
  (f : C(α, β)) (a : α), (BoundedContinuousFunction.mkOfCompact f) a = f a
-- Mathlib.Data.Fintype.Defs
/-- A proof that `elems` contains every element of the type  -/
Fintype.complete : ∀ {α : Type u_4} [self : Fintype α] (x : α), x ∈ Fintype.elems
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremKind.bwd.injEq : ∀ (gen gen_1 : Bool),
  (Lean.Meta.Grind.EMatchTheoremKind.bwd gen = Lean.Meta.Grind.EMatchTheoremKind.bwd gen_1) = (gen = gen_1)
-- Mathlib.Topology.Bases
TopologicalSpace.IsTopologicalBasis.continuousOn_iff : ∀ {α : Type u} {β : Type u_1} [t : TopologicalSpace α] {s : Set α} [inst : TopologicalSpace β] {B : Set (Set β)},
  TopologicalSpace.IsTopologicalBasis B →
    ∀ {f : α → β}, ContinuousOn f s ↔ ∀ t_1 ∈ B, ∃ u, IsOpen u ∧ f ⁻¹' t_1 ∩ s = u ∩ s
-- Init.Data.Bool
Bool.if_false_left : ∀ (p : Prop) [h : Decidable p] (f : Bool), (if p then false else f) = (!decide p && f)
-- Mathlib.Tactic.Push
/-- Try to rewrite using a `push` lemma.  -/
Mathlib.Tactic.Push.pushStep : Mathlib.Tactic.Push.Head → Mathlib.Tactic.Push.Config → Lean.Meta.Simp.Simproc
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k},
      List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
        ⟨k, v⟩ ∈ l → ∀ {h' : k' ∈ t.insertMany l}, (t.insertMany l).get k' h' = cast ⋯ v
-- Mathlib.Topology.Constructions
IsOpenMap.subtype_mk : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {p : X → Prop} {f : Y → X},
  IsOpenMap f → ∀ (hp : ∀ (x : Y), p (f x)), IsOpenMap fun x => ⟨f x, ⋯⟩
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.mem_inf : ∀ {K : Type u} [inst : DivisionRing K] {p p' : Subfield K} {x : K}, x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
/-- An n-ary version of `Set.add_mem_add`.  -/
Set.multiset_sum_mem_multiset_sum : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] (t : Multiset ι) (f : ι → Set α) (g : ι → α),
  (∀ i ∈ t, g i ∈ f i) → (Multiset.map g t).sum ∈ (Multiset.map f t).sum
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.ResidueField.finite_of_module_finite : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : IsLocalRing R] [inst_2 : CommRing S]
  [inst_3 : IsLocalRing S] [inst_4 : Algebra R S] [inst_5 : IsLocalHom (algebraMap R S)] [Module.Finite R S],
  Module.Finite (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S)
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.of_smul : ∀ {Γ : Type u_1} {R : Type u_3} {V : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid V]
  [inst_2 : SMulZeroClass R V] (r : R) (x : HahnSeries Γ V), (HahnModule.of R) (r • x) = r • (HahnModule.of R) x
-- Mathlib.LinearAlgebra.Transvection.Generation
_private.Mathlib.LinearAlgebra.Transvection.Generation.0.LinearEquiv.auxTransvection_fixed : ∀ {K : Type u_1} [inst : DivisionRing K] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module K V] {e : V ≃ₗ[K] V}
  {f : Module.Dual K V} {u : V} (hf : (↑e).fixedSubmodule ⊔ K ∙ (e u - u) ≤ LinearMap.ker f),
  (↑e).fixedSubmodule ≤ (↑(LinearEquiv.auxTransvection✝ hf)).fixedSubmodule
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.subtypeVal_apply : ∀ {β : Type u_3} [inst : SemilatticeInf β] [inst_1 : OrderTop β] {P : β → Prop} (Ptop : P ⊤)
  (Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)) (x : { x // P x }), (InfTopHom.subtypeVal Ptop Pinf) x = ↑x
-- Mathlib.Algebra.Group.Basic
mul_eq_left : ∀ {M : Type u_4} [inst : Monoid M] [IsLeftCancelMul M] {a b : M}, a * b = a ↔ b = 1
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.union.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β),
  m₁.union m₂ = if (↑m₁).size ≤ (↑m₂).size then ↑(m₂.insertManyIfNew ↑m₁) else ↑(m₁.insertMany ↑m₂)
-- Init.Data.SInt.Bitwise
Int32.toBitVec_xor : ∀ (a b : Int32), (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.forgetToRingCat_obj : ∀ {R : CommRingCat}, ↑((CategoryTheory.forget₂ CommRingCat RingCat).obj R) = ↑R
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- The image under an `AddMonoidHom` of the `AddSubmonoid` generated by a set equals the
`AddSubmonoid` generated by the image of the set.  -/
AddMonoidHom.map_mclosure : ∀ {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) (s : Set M),
  AddSubmonoid.map f (AddSubmonoid.closure s) = AddSubmonoid.closure (⇑f '' s)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.findEntry?_insert_of_eq : ∀ {α : Type u_1} {cmp : α → α → Ordering} {β : Type u_2} {k' k : α} {v : β} [Std.TransCmp cmp]
  (t : RBTree.RBMap α β cmp), cmp k' k = Ordering.eq → (t.insert k v).findEntry? k' = some (k, v)
-- Mathlib.Analysis.SpecialFunctions.Log.Summable
Summable.summable_log_norm_one_add : ∀ {ι : Type u_1} {R : Type u_2} [inst : NormedCommRing R] [NormOneClass R] {f : ι → R},
  (Summable fun n => ‖f n‖) → Summable fun i => Real.log ‖1 + f i‖
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- For `f : α →ᵤ[𝔖] β`, where `𝔖 : Set (Set α)` is nonempty and directed, `𝓝 f` admits the
family `{g | ∀ x ∈ S, (f x, g x) ∈ V}` for `S ∈ 𝔖` and `V ∈ 𝓤 β` as a filter basis.  -/
UniformOnFun.hasBasis_nhds : ∀ (α : Type u_1) (β : Type u_2) [inst : UniformSpace β] (𝔖 : Set (Set α)) (f : UniformOnFun α β 𝔖),
  𝔖.Nonempty →
    DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖 →
      (nhds f).HasBasis (fun SV => SV.1 ∈ 𝔖 ∧ SV.2 ∈ uniformity β) fun SV => {g | (g, f) ∈ UniformOnFun.gen 𝔖 SV.1 SV.2}
-- Mathlib.Algebra.Ring.Parity
Nat.mod_two_add_succ_mod_two : ∀ (m : ℕ), m % 2 + (m + 1) % 2 = 1
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFraction.map_ofInv_hom_id : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (W : CategoryTheory.MorphismProperty C) {X Y : C} (s : Y ⟶ X)
  (hs : W s) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.RightFraction.ofInv s hs).map L hL) (L.map s) =
    CategoryTheory.CategoryStruct.id (L.obj X)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- Uses `left` co(ntra)variant.  -/
Left.neg_nonpos_iff : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddLeftMono α] {a : α}, -a ≤ 0 ↔ 0 ≤ a
-- Mathlib.RingTheory.Artinian.Module
Ring.isArtinian_of_zero_eq_one : ∀ {R : Type u_1} [inst : Semiring R], 0 = 1 → IsArtinianRing R
-- Lean.Declaration
Lean.Declaration.opaqueDecl.inj : ∀ {val val_1 : Lean.OpaqueVal}, Lean.Declaration.opaqueDecl val = Lean.Declaration.opaqueDecl val_1 → val = val_1
-- Mathlib.Topology.Order.IntermediateValue
intermediate_value_Ioc' : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a b : α}, a ≤ b → ∀ {f : α → δ}, ContinuousOn f (Set.Icc a b) → Set.Ico (f b) (f a) ⊆ f '' Set.Ioc a b
-- Lean.Meta.Basic
/-- Given `e` of the form `fun (a_1 : A_1) ... (a_n : A_n) => t[a_1, ..., a_n]` and `p_1 : A_1, ... p_n : A_n`, return `t[p_1, ..., p_n]`.
It uses `whnf` to reduce `e` if it is not a lambda  -/
Lean.Meta.instantiateLambda : Lean.Expr → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Data.Finset.Basic
Equiv.piFinsetUnion_right : ∀ {ι : Type u_5} [inst : DecidableEq ι] (α : ι → Type u_4) {s t : Finset ι} (h : Disjoint s t) {f : (i : ↥s) → α ↑i}
  {g : (i : ↥t) → α ↑i} {i : ι} (hi : i ∈ t) (hi' : i ∈ s ∪ t), (Equiv.piFinsetUnion α h) (f, g) ⟨i, hi'⟩ = g ⟨i, hi⟩
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.restoreM_refl : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α : Type u}
  {post : α → Pred} {epost : EPred} (x : stM m m α),
  ⦃ Std.Internal.Do.wp (pure x) post epost ⦄ restoreM x ⦃ post; epost ⦄
-- Mathlib.Order.Interval.Set.ProjIcc
Set.coe_projIic : ∀ {α : Type u_1} [inst : LinearOrder α] (b x : α), ↑(Set.projIic b x) = min b x
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.not_matchesAt_or_isLongestMatchAt_skipPrefixWhile : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  (s : String.Slice),
  ¬String.Slice.Pattern.Model.MatchesAt pat (s.skipPrefixWhile pat) ∨
    String.Slice.Pattern.Model.IsLongestMatchAt pat (s.skipPrefixWhile pat) (s.skipPrefixWhile pat)
-- Mathlib.Topology.Algebra.Monoid
/-- The (topological-space) closure of an additive submonoid of a space `M` with
`ContinuousAdd` is itself an additive submonoid.  -/
AddSubsemigroup.topologicalClosure : {M : Type u_3} →
  [inst : TopologicalSpace M] →
    [inst_1 : AddSemigroup M] → [SeparatelyContinuousAdd M] → AddSubsemigroup M → AddSubsemigroup M
-- Mathlib.Data.Set.Disjoint
Set.disjoint_right : ∀ {α : Type u} {s t : Set α}, Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ t → a ∉ s
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
/-- `SymRel` as a ring congruence, used to build the quotient.  -/
TensorAlgebra.symRingCon : (R : Type u_1) →
  (M : Type u_2) →
    [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → RingCon (TensorAlgebra R M)
-- Mathlib.CategoryTheory.Limits.VanKampen
CategoryTheory.IsVanKampenColimit.whiskerEquivalence : ∀ {J : Type v'} [inst : CategoryTheory.Category.{u', v'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {K : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} K] (e : J ≌ K) {F : CategoryTheory.Functor K C}
  {c : CategoryTheory.Limits.Cocone F},
  CategoryTheory.IsVanKampenColimit c →
    CategoryTheory.IsVanKampenColimit (CategoryTheory.Limits.Cocone.whisker e.functor c)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.lt_zpow_of_log_lt : ∀ {x y : ℝ} {n : ℤ}, 0 < y → Real.log x < ↑n * Real.log y → x < y ^ n
-- Mathlib.Algebra.Category.CommBialgCat
_private.Mathlib.Algebra.Category.CommBialgCat.0.CommBialgCat.Hom.mk.injEq : ∀ {R : Type u} [inst : CommRing R] {A B : CommBialgCat R} (hom' hom'_1 : ↑A →ₐc[R] ↑B),
  ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_image_of_injOn : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β}, Set.InjOn f s → Nat.card ↑(f '' s) = Nat.card ↑s
-- Mathlib.LinearAlgebra.Matrix.Stochastic
/-- A square matrix is row stochastic iff all entries are nonnegative, and right
multiplication by the vector of all 1s gives the vector of all 1s.  -/
Matrix.rowStochastic : (R : Type u_3) →
  (n : Type u_4) →
    [inst : Fintype n] →
      [inst_1 : DecidableEq n] →
        [inst_2 : Semiring R] → [inst_3 : PartialOrder R] → [IsOrderedRing R] → Submonoid (Matrix n n R)
-- Mathlib.Probability.Independence.BoundedContinuousFunction
process_indepFun_of_bcf : ∀ {Ω : Type u_1} {S : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : S → Type u_4} {H : Type u_7}
  [inst : (s : S) → TopologicalSpace (E s)] [inst_1 : (s : S) → MeasurableSpace (E s)] [∀ (s : S), BorelSpace (E s)]
  [∀ (s : S), HasOuterApproxClosed (E s)] [inst_4 : TopologicalSpace H] [inst_5 : MeasurableSpace H] [BorelSpace H]
  [HasOuterApproxClosed H] {X : (s : S) → Ω → E s} {U : Ω → H} [MeasureTheory.IsZeroOrProbabilityMeasure P],
  (∀ (s : S), AEMeasurable (X s) P) →
    AEMeasurable U P →
      (∀ (I : Finset S) (f : BoundedContinuousFunction ((s : ↥I) → E ↑s) ℝ) (g : BoundedContinuousFunction H ℝ),
          ∫ (x : Ω), (fun ω => (f fun x => X (↑x) ω) * g (U ω)) x ∂P =
            (∫ (x : Ω), (fun ω => f fun x => X (↑x) ω) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P) →
        ProbabilityTheory.IndepFun (fun ω s => X s ω) U P
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.norm_compContinuous_le : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
  [inst_2 : TopologicalSpace γ] (f : BoundedContinuousFunction α β) (g : C(γ, α)), ‖f.compContinuous g‖ ≤ ‖f‖
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
one_lt_of_lt_mul_left : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : LT α] [MulRightReflectLT α] {a b : α}, b < a * b → 1 < a
-- Mathlib.Algebra.Group.Subgroup.Even
Subsemigroup.coe_square : ∀ {S : Type u_1} [inst : CommSemigroup S], ↑(Subsemigroup.square S) = {s | IsSquare s}
-- Lean.Meta.Match.Basic
Lean.Meta.Match.AltLHS.mk.inj : ∀ {ref : Lean.Syntax} {fvarDecls : List Lean.LocalDecl} {patterns : List Lean.Meta.Match.Pattern} {ref_1 : Lean.Syntax}
  {fvarDecls_1 : List Lean.LocalDecl} {patterns_1 : List Lean.Meta.Match.Pattern},
  { ref := ref, fvarDecls := fvarDecls, patterns := patterns } =
      { ref := ref_1, fvarDecls := fvarDecls_1, patterns := patterns_1 } →
    ref = ref_1 ∧ fvarDecls = fvarDecls_1 ∧ patterns = patterns_1
-- Mathlib.Order.WithBot
WithBot.unbotA_mono : ∀ {α : Type u_1} [inst : LE α] {x y : WithBot α} [inst_1 : Nonempty α], x ≠ ⊥ → x ≤ y → x.unbotA ≤ y.unbotA
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
/-- The closure of a submodule as a closed submodule.  -/
Submodule.closure : {R : Type u_2} →
  {M : Type u_3} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : TopologicalSpace M] →
          [inst_3 : Module R M] → [ContinuousAdd M] → [ContinuousConstSMul R M] → Submodule R M → ClosedSubmodule R M
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- Return syntax for the rewrite tactic `rw [e]`.  -/
Mathlib.Tactic.LibraryRewrite.mkRewrite : Option ℕ → Bool → Lean.Term → Option Lean.Name → Lean.CoreM (Lean.TSyntax `tactic)
-- Lean.Elab.Tactic.Location
/-- `hypotheses` are hypothesis names in the main goal that the tactic should be applied to.
If `type` is true, then the tactic should also be applied to the target type.  -/
Lean.Elab.Tactic.Location.targets : Array Lean.Syntax → Bool → Lean.Elab.Tactic.Location
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_dvd_right_split_ineq_cert.eq_1 : ∀ (p₁ p₂ : Int.Internal.Linear.Poly) (k a : ℤ) (p' : Int.Internal.Linear.Poly),
  Int.Internal.Linear.cooper_dvd_right_split_ineq_cert p₁ p₂ k a p' =
    (p₁.leadCoeff.beq' a).and'
      (p'.beq' ((Int.Internal.Linear.Poly.combine_mul_k p₂.leadCoeff (-a) p₁.tail p₂.tail).addConst_k (-a * k)))
-- Mathlib.Order.Heyting.Basic
Prod.instSDiff : {α : Type u_2} → {β : Type u_3} → [SDiff α] → [SDiff β] → SDiff (α × β)
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.restrictionLT_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : PartialOrder J] {j : J}
  (F : CategoryTheory.Functor (↑(Set.Iic j)) C) {i : J} (hi : i ≤ j) (k : J) (hk : k < i),
  (CategoryTheory.SmallObject.restrictionLT F hi).obj ⟨k, hk⟩ = F.obj ⟨k, ⋯⟩
-- Mathlib.LinearAlgebra.Matrix.Reindex
Matrix.symm_reindexLinearEquiv : ∀ {m : Type u_2} {n : Type u_3} {m' : Type u_6} {n' : Type u_7} (R : Type u_11) (A : Type u_12) [inst : Semiring R]
  [inst_1 : AddCommMonoid A] [inst_2 : Module R A] (eₘ : m ≃ m') (eₙ : n ≃ n'),
  (Matrix.reindexLinearEquiv R A eₘ eₙ).symm = Matrix.reindexLinearEquiv R A eₘ.symm eₙ.symm
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.DiagnosticTag.noConfusionType : Sort v✝ → Lean.Lsp.DiagnosticTag → Lean.Lsp.DiagnosticTag → Sort v✝
-- Mathlib.AlgebraicGeometry.PointsPi
AlgebraicGeometry.pointsPi_surjective_of_isAffine : ∀ {ι : Type u} (R : ι → CommRingCat) (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X],
  Function.Surjective (AlgebraicGeometry.pointsPi R X)
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.Iteration.congr_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J]
  [inst_4 : CategoryTheory.Limits.HasIterationOfShape J C] [inst_5 : WellFoundedLT J] {j₁ j₂ : J}
  (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) {k₁ k₂ : J} (h : k₁ ≤ k₂) (h₁ : k₂ ≤ j₁) (h₂ : k₂ ≤ j₂),
  iter₁.F.map (CategoryTheory.homOfLE h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp (iter₂.F.map (CategoryTheory.homOfLE h)) (CategoryTheory.eqToHom ⋯))
-- Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Besicovitch.SatelliteConfig.exists_normalized_aux3 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {N : ℕ} {τ : ℝ}
  (a : Besicovitch.SatelliteConfig E N τ),
  a.c (Fin.last N) = 0 →
    a.r (Fin.last N) = 1 →
      1 ≤ τ →
        ∀ (δ : ℝ),
          τ ≤ 1 + δ / 4 →
            ∀ (i j : Fin N.succ),
              i ≠ j → 2 < ‖a.c i‖ → ‖a.c i‖ ≤ ‖a.c j‖ → 1 - δ ≤ ‖(2 / ‖a.c i‖) • a.c i - (2 / ‖a.c j‖) • a.c j‖
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.disjoint_def' : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {p p' : Submodule R M}, Disjoint p p' ↔ ∀ x ∈ p, ∀ y ∈ p', x = y → x = 0
-- Mathlib.Data.Fin.Basic
Fin.ne_last_of_lt : ∀ {n : ℕ} {a b : Fin (n + 1)}, a < b → a ≠ Fin.last n
-- Mathlib.LinearAlgebra.TensorProduct.Pi
/-- For any `R`-module `N` and finite index type `ι`, `N ⊗[R] (ι → R)` is canonically
isomorphic to `ι → N`.  -/
TensorProduct.piScalarRight : (R : Type u_1) →
  [inst : CommSemiring R] →
    (S : Type u_2) →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          (N : Type u_3) →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] →
                [inst_5 : Module S N] →
                  [inst_6 : IsScalarTower R S N] →
                    (ι : Type u_4) → [Fintype ι] → [DecidableEq ι] → TensorProduct R N (ι → R) ≃ₗ[S] ι → N
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.map_fst_darts : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v),
  List.map (fun x => x.toProd.1) p.darts = p.support.dropLast
-- Mathlib.Algebra.Ring.Divisibility.Basic
MulEquiv.decompositionMonoid : ∀ {α : Type u_1} {β : Type u_2} [inst : Semigroup α] [inst_1 : Semigroup β] {F : Type u_3} [inst_2 : EquivLike F α β]
  [MulEquivClass F α β] (f : F) [DecompositionMonoid β], DecompositionMonoid α
-- Mathlib.Data.Set.NAry
Set.image_subset_image2_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {b : β},
  b ∈ t → (fun a => f a b) '' s ⊆ Set.image2 f s t
-- Mathlib.Topology.Algebra.ConstMulAction
closure_smul₀ : ∀ {G₀ : Type u_4} [inst : GroupWithZero G₀] {E : Type u_5} [inst_1 : Zero E] [inst_2 : MulActionWithZero G₀ E]
  [inst_3 : TopologicalSpace E] [T1Space E] [ContinuousConstSMul G₀ E] (c : G₀) (s : Set E),
  closure (c • s) = c • closure s
-- Std.Sat.AIG.RelabelNat
/-- `relabelNat` preserves unsatisfiablility.
 -/
Std.Sat.AIG.Entrypoint.relabelNat_unsat_iff : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {entry : Std.Sat.AIG.Entrypoint α},
  entry.relabelNat.Unsat ↔ entry.Unsat
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_iff_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {k : α},
  t.contains k = true ↔ k ∈ t
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.union_neg : ∀ {α : Type u_2} [inst : Neg α] {s t : Set α}, -(s ∪ t) = -s ∪ -t
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.eval₂_const_pUnitAlgEquiv_symm : ∀ {R : Type u_2} {S : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] {f : Polynomial R} {φ : R →+* S}
  {a : S}, MvPolynomial.eval₂ φ (fun x => a) ((MvPolynomial.pUnitAlgEquiv R).symm f) = Polynomial.eval₂ φ a f
-- Std.Http.Data.URI.Basic
Std.Http.URI.UserInfo.mk.inj : ∀ {username : Std.Http.URI.EncodedUserInfo} {password : Option Std.Http.URI.EncodedUserInfo}
  {username_1 : Std.Http.URI.EncodedUserInfo} {password_1 : Option Std.Http.URI.EncodedUserInfo},
  { username := username, password := password } = { username := username_1, password := password_1 } →
    username = username_1 ∧ password = password_1
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof.core : Lean.Expr → Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr → Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof
-- Mathlib.SetTheory.Cardinal.Free
Cardinal.mk_freeRing : ∀ (α : Type u), Cardinal.mk (FreeRing α) = max (Cardinal.mk α) Cardinal.aleph0
-- Std.Tactic.BVDecide.Normalize.Canonicalize
Std.Tactic.BVDecide.Normalize.BitVec.or_elim : ∀ {w : ℕ} (x y : BitVec w), x ||| y = ~~~(~~~x &&& ~~~y)
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.isLocalHom_singleZeroAlgHom : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddMonoid M], IsLocalHom AddMonoidAlgebra.singleZeroAlgHom
-- Mathlib.Logic.Basic
Iff.not_right : ∀ {a b : Prop}, (¬a ↔ b) → (a ↔ ¬b)
-- Mathlib.Algebra.Category.Ring.Adjunctions
CommRingCat.free_obj_coe : ∀ {α : Type u}, ↑(CommRingCat.free.obj α) = MvPolynomial α ℤ
-- Batteries.Data.PairingHeap
_private.Batteries.Data.PairingHeap.0.Batteries.PairingHeapImp.Heap.size.match_1.eq_1 : ∀ {α : Type u_1} (motive : Batteries.PairingHeapImp.Heap α → Sort u_2)
  (h_1 : Unit → motive Batteries.PairingHeapImp.Heap.nil)
  (h_2 : (a : α) → (c s : Batteries.PairingHeapImp.Heap α) → motive (Batteries.PairingHeapImp.Heap.node a c s)),
  (match Batteries.PairingHeapImp.Heap.nil with
    | Batteries.PairingHeapImp.Heap.nil => h_1 ()
    | Batteries.PairingHeapImp.Heap.node a c s => h_2 a c s) =
    h_1 ()
-- Mathlib.Topology.Basic
IsOpen.isLocallyClosed : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], IsOpen s → IsLocallyClosed s
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.toList_cons : ∀ {α : Type u_1} (x : α) (xs : FreeMonoid α), FreeMonoid.toList (x :: xs) = x :: FreeMonoid.toList xs
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.ComputableSmall.deflate : {α : Type v} → [self : Std.Internal.ComputableSmall α] → α → Std.Internal.ComputableSmall.Target α
-- Mathlib.Tactic.FBinop
FBinopElab.SRec.mk.sizeOf_spec : ∀ (name : Lean.Name) (args : Array Lean.Expr), sizeOf { name := name, args := args } = 1 + sizeOf name + sizeOf args
-- Mathlib.LinearAlgebra.Determinant
LinearMap.det_map : ∀ {K : Type u_5} {V : Type u_6} {W : Type u_7} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup W] [inst_4 : Module K W] {F : Type u_8}
  [inst_5 : EquivLike F (Module.End K V) (Module.End K W)] [AlgEquivClass F K (Module.End K V) (Module.End K W)] (f : F)
  (x : Module.End K V), LinearMap.det (f x) = LinearMap.det x
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂_map_app_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f : X ⟶ Y) (Y_1 X_1 : C),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂ C).map f).app Y_1).app X_1 =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X_1) Y_1