mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Compactification.OnePoint.Basic
Homeomorph.onePointCongr_symm_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) (a : OnePoint Y),
  h.onePointCongr.symm a = OnePoint.map (⇑h.symm) a
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_add_card_nsmul : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : AddCommMonoid M] {f : ι → M} {b : M},
  ∑ a ∈ s, f a + s.card • b = ∑ a ∈ s, (f a + b)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_union_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k fallback : α}, k ∉ t₁ → (t₁ ∪ t₂).getD k fallback = t₂.getD k fallback
-- Lean.Elab.Tactic.Conv.Basic
Lean.Elab.Tactic.Conv.evalWhnf : Lean.Elab.Tactic.Tactic
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_inter_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α} {fallback : β}, k ∉ t₂ → Std.DTreeMap.Const.getD (t₁ ∩ t₂) k fallback = fallback
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.characteristic_iff_map_eq : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G},
  H.Characteristic ↔ ∀ (ϕ : G ≃+ G), AddSubgroup.map ϕ.toAddMonoidHom H = H
-- Mathlib.Topology.Algebra.Group.Torsor
ContinuousOn.vsub : ∀ {V : Type u_1} {P : Type u_2} {α : Type u_3} [inst : AddGroup V] [inst_1 : TopologicalSpace V]
  [inst_2 : AddTorsor V P] [inst_3 : TopologicalSpace P] [IsTopologicalAddTorsor P] [inst_5 : TopologicalSpace α]
  {f g : α → P} {s : Set α}, ContinuousOn f s → ContinuousOn g s → ContinuousOn (fun x => f x -ᵥ g x) s
-- Mathlib.AlgebraicGeometry.FunctionField
/-- The restriction map from a component to the function field.  -/
AlgebraicGeometry.Scheme.germToFunctionField : (X : AlgebraicGeometry.Scheme) →
  [inst : IrreducibleSpace ↥X] → (U : X.Opens) → [h : Nonempty ↥↑U] → X.presheaf.obj (Opposite.op U) ⟶ X.functionField
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
CategoryTheory.PreZeroHypercover.Relation.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {S : C} {E : CategoryTheory.PreZeroHypercover S}
  {i j : E.I₀} {obj : C} {fst : obj ⟶ E.X i} {snd : obj ⟶ E.X j}
  {w : CategoryTheory.CategoryStruct.comp fst (E.f i) = CategoryTheory.CategoryStruct.comp snd (E.f j)} {obj_1 : C}
  {fst_1 : obj_1 ⟶ E.X i} {snd_1 : obj_1 ⟶ E.X j}
  {w_1 : CategoryTheory.CategoryStruct.comp fst_1 (E.f i) = CategoryTheory.CategoryStruct.comp snd_1 (E.f j)},
  { obj := obj, fst := fst, snd := snd, w := w } = { obj := obj_1, fst := fst_1, snd := snd_1, w := w_1 } →
    obj = obj_1 ∧ fst ≍ fst_1 ∧ snd ≍ snd_1
-- Init.Data.UInt.Lemmas
UInt16.ofNatClamp_toNat : ∀ (n : UInt16), UInt16.ofNatClamp n.toNat = n
-- Init.Data.Iterators.Basic
Std.Iter.mk.sizeOf_spec : ∀ {α β : Type w} [inst : SizeOf α] [inst_1 : SizeOf β] (internalState : α),
  sizeOf { internalState := internalState } = 1 + sizeOf internalState
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithLowerSet.toLowerSet_specializes_toLowerSet : ∀ {α : Type u_1} [inst : Preorder α] {a b : α},
  Topology.WithLowerSet.toLowerSet a ⤳ Topology.WithLowerSet.toLowerSet b ↔ a ≤ b
-- Init.Data.Int.DivMod.Bootstrap
Int.zero_emod : ∀ (b : ℤ), 0 % b = 0
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.instInhabited : Inhabited YoungDiagram
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.instCategoryStruct : (J : Type u_1) →
  [inst : LinearOrder J] → CategoryTheory.CategoryStruct.{u_1, u_1} (CategoryTheory.SimplicialThickening J)
-- Mathlib.NumberTheory.ModularForms.NormTrace
instMulActionSubtypeGeneralLinearGroupFinOfNatNatRealMemSubgroup : {ℋ : Subgroup (GL (Fin 2) ℝ)} → MulAction ↥ℋ ↥ℋ
-- Init.Data.Option.Lemmas
Option.isSome_right_of_isSome_min : ∀ {α : Type u_1} [inst : Min α] {o o' : Option α}, (o ⊓ o').isSome = true → o'.isSome = true
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.algebra' : {R' : Type u_4} →
  {K : Type u_5} →
    {L : Type u_6} →
      [inst : Field K] →
        [inst_1 : Field L] →
          [inst_2 : Algebra K L] →
            (S : IntermediateField K L) →
              [inst_3 : CommSemiring R'] →
                [inst_4 : SMul R' K] → [inst_5 : Algebra R' L] → [IsScalarTower R' K L] → Algebra R' ↥S
-- Mathlib.Algebra.Group.WithOne.Basic
/-- Lift an additive semigroup homomorphism `f` to a bundled additive monoid homomorphism.  -/
WithZero.lift : {α : Type u} → {β : Type v} → [inst : Add α] → [inst_1 : AddZeroClass β] → (α →ₙ+ β) ≃ (WithZero α →+ β)
-- Mathlib.Order.Lattice
sup_le_iff : ∀ {α : Type u} [inst : SemilatticeSup α] {a b c : α}, a ⊔ b ≤ c ↔ a ≤ c ∧ b ≤ c
-- Lean.Meta.Tactic.Grind.Util
/-- Instantiates metavariables occurring in the target and hypotheses.
 -/
Lean.MVarId.instantiateGoalMVars : Lean.MVarId → Lean.MetaM Lean.MVarId
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- Store the current recursive call and its context.  -/
Lean.Elab.WF.GuessLex.RecCallWithContext.create : Lean.Syntax → ℕ → Array Lean.Expr → ℕ → Array Lean.Expr → Lean.MetaM Lean.Elab.WF.GuessLex.RecCallWithContext
-- Mathlib.Algebra.Field.Subfield.Defs
/-- A subfield is closed under inverses.  -/
Subfield.inv_mem : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K) {x : K}, x ∈ s → x⁻¹ ∈ s
-- Init.Data.Vector.Lemmas
/-- Reversing a flatten is the same as reversing the order of parts and reversing all parts.  -/
Vector.reverse_flatten : ∀ {α : Type u_1} {m n : ℕ} {xss : Vector (Vector α m) n},
  xss.flatten.reverse = (Vector.map Vector.reverse xss).reverse.flatten
-- Mathlib.Order.UpperLower.Closure
lowerClosure_union : ∀ {α : Type u_1} [inst : Preorder α] (s t : Set α), lowerClosure (s ∪ t) = lowerClosure s ⊔ lowerClosure t
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.coe_symm_mk : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (g : β → α) (s : Set α) (t : Set β) (ml : ∀ ⦃x : α⦄, x ∈ s → f x ∈ t)
  (mr : ∀ ⦃x : β⦄, x ∈ t → g x ∈ s) (il : ∀ ⦃x : α⦄, x ∈ s → g (f x) = x) (ir : ∀ ⦃x : β⦄, x ∈ t → f (g x) = x),
  ↑{ toFun := f, invFun := g, source := s, target := t, map_source' := ml, map_target' := mr, left_inv' := il,
          right_inv' := ir }.symm =
    g
-- Mathlib.Algebra.Homology.HomotopyCategory
/-- The obvious isomorphism between
`HomotopyCategory.quotient V c ⋙ F.mapHomotopyCategory c` and
`F.mapHomologicalComplex c ⋙ HomotopyCategory.quotient W c` when `F : V ⥤ W` is
an additive functor.  -/
CategoryTheory.Functor.mapHomotopyCategoryFactors : {ι : Type u_2} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {W : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_1, u_3} W] →
            [inst_3 : CategoryTheory.Preadditive W] →
              (F : CategoryTheory.Functor V W) →
                [inst_4 : F.Additive] →
                  (c : ComplexShape ι) →
                    (HomotopyCategory.quotient V c).comp (F.mapHomotopyCategory c) ≅
                      (F.mapHomologicalComplex c).comp (HomotopyCategory.quotient W c)
-- Mathlib.Combinatorics.SetFamily.Compression.Down
Finset.memberSubfamily_union : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (𝒜 ℬ : Finset (Finset α)),
  Finset.memberSubfamily a (𝒜 ∪ ℬ) = Finset.memberSubfamily a 𝒜 ∪ Finset.memberSubfamily a ℬ
-- Init.Data.List.Lemmas
List.map_eq_cons_iff : ∀ {α : Type u_1} {β : Type u_2} {b : β} {l₂ : List β} {f : α → β} {l : List α},
  List.map f l = b :: l₂ ↔ ∃ a l₁, l = a :: l₁ ∧ f a = b ∧ List.map f l₁ = l₂
-- Mathlib.Geometry.Convex.Cone.Face.Basic
PointedCone.IsFaceOf.mem_of_smul_add_mem : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {F C : PointedCone R M},
  F.IsFaceOf C → ∀ {x y : M} {a : R}, x ∈ C → y ∈ C → 0 < a → a • x + y ∈ F → x ∈ F
-- Mathlib.LinearAlgebra.Basis.VectorSpace
Module.Basis.ofVectorSpaceIndex.linearIndependent : ∀ (K : Type u_3) (V : Type u_4) [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  LinearIndependent K Subtype.val
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.map_prodMkRight : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {δ : Type u_4}
  {mδ : MeasurableSpace δ} (κ : ProbabilityTheory.Kernel α β) (γ : Type u_5) {mγ : MeasurableSpace γ} (f : β → δ),
  (ProbabilityTheory.Kernel.prodMkRight γ κ).map f = ProbabilityTheory.Kernel.prodMkRight γ (κ.map f)
-- Mathlib.Order.Hom.Lattice
InfHom.comp_id : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Min β] (f : InfHom α β), f.comp (InfHom.id α) = f
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instAdd : {α : Type u} →
  {R : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : PseudoMetricSpace R] →
        [inst_2 : Add R] → [BoundedAdd R] → [ContinuousAdd R] → Add (BoundedContinuousFunction α R)
-- Lean.Meta.Tactic.Grind.Cases
/-- Removes the given declaration from `s`.  -/
Lean.Meta.Grind.CasesTypes.erase : Lean.Meta.Grind.CasesTypes → Lean.Name → Lean.Meta.Grind.CasesTypes
-- Mathlib.Algebra.GradedMonoid
GradedMonoid.mk_pow : ∀ {ι : Type u_1} (A : ι → Type u_2) [inst : AddMonoid ι] [inst_1 : GradedMonoid.GMonoid A] {i : ι} (a : A i) (n : ℕ),
  GradedMonoid.mk i a ^ n = GradedMonoid.mk (n • i) (GradedMonoid.GMonoid.gnpow n a)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.negDvdTight.sizeOf_spec : ∀ (c₁ : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr) (c₂ : Lean.Meta.Grind.Arith.Cutsat.LeCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.negDvdTight c₁ c₂) = 1 + sizeOf c₁ + sizeOf c₂
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
EReal.instMeasurableMul₂ : MeasurableMul₂ EReal
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (not_mem : k ∉ t₁) {h' : k ∈ t₁ ∪ t₂}, (t₁ ∪ t₂)[k] = t₂[k]
-- Mathlib.Algebra.Group.EvenFunction
/-- **Alias** of `Function.Odd.finsetSum_eq_zero`.

---

The sum of values of an odd function over a symmetric finite set is zero.  -/
Function.Odd.finset_sum_eq_zero : ∀ {α : Type u_3} {β : Type u_4} [inst : AddCommGroup β] [IsAddTorsionFree β] [inst_2 : InvolutiveNeg α] {f : α → β},
  Function.Odd f → ∀ {s : Finset α}, Finset.map (Equiv.toEmbedding (Equiv.neg α)) s = s → s.sum f = 0
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.extend.congr_simp : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] {δ : Type u_2}
  [inst_2 : TopologicalSpace δ] [inst_3 : DiscreteTopology δ] (f f_1 : α ↪ δ),
  f = f_1 →
    ∀ (g g_1 : BoundedContinuousFunction α β),
      g = g_1 →
        ∀ (h h_1 : BoundedContinuousFunction δ β),
          h = h_1 → BoundedContinuousFunction.extend f g h = BoundedContinuousFunction.extend f_1 g_1 h_1
-- Mathlib.Algebra.Free
FreeMagma.instMul.eq_1 : ∀ {α : Type u}, FreeMagma.instMul = { mul := FreeMagma.mul }
-- Mathlib.GroupTheory.Coset.Basic
/-- If `s ≤ t`, there is an embedding `s ⧸ H.addSubgroupOf s ↪ t ⧸ H.addSubgroupOf t`.  -/
AddSubgroup.quotientAddSubgroupOfEmbeddingOfLE : {α : Type u_1} →
  [inst : AddGroup α] →
    {s t : AddSubgroup α} → (H : AddSubgroup α) → s ≤ t → ↥s ⧸ H.addSubgroupOf s ↪ ↥t ⧸ H.addSubgroupOf t
-- Mathlib.Algebra.Group.Hom.Instances
MonoidHom.flipHom.eq_1 : ∀ {M : Type uM} {N : Type uN} {P : Type uP} {x : MulOneClass M} {x_1 : MulOneClass N} {x_2 : CommMonoid P},
  MonoidHom.flipHom = { toFun := MonoidHom.flip, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Analysis.Calculus.DSlope
sub_smul_dslope_of_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {a : 𝕜}, f a = 0 → ∀ (b : 𝕜), (b - a) • dslope f a b = f b
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.map_comp_eq_zero_iff_of_epi_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] [L.IsLocalization P.isoModSerre] [inst_5 : CategoryTheory.Preadditive D] [L.Additive]
  {X Z Y : C} (f : X ⟶ Z) (g : Z ⟶ Y) [CategoryTheory.Epi f] [CategoryTheory.Mono g],
  CategoryTheory.CategoryStruct.comp (L.map f) (L.map g) = 0 ↔ P Z
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.Lex.addRightStrictMono : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → AddMonoid (α i)]
  [inst_2 : (i : ι) → LinearOrder (α i)] [∀ (i : ι), AddRightStrictMono (α i)],
  AddRightStrictMono (Lex (Π₀ (i : ι), α i))
-- Mathlib.Order.Heyting.Basic
/-- Transfer `BiheytingAlgebra` across an `Equiv`.  -/
Equiv.biheytingAlgebra : {α : Type u_2} → {β : Type u_3} → α ≃ β → [BiheytingAlgebra β] → BiheytingAlgebra α
-- Mathlib.Algebra.Order.Group.Indicator
Set.one_le_mulIndicator_apply : ∀ {α : Type u_2} {M : Type u_3} [inst : Preorder M] [inst_1 : One M] {s : Set α} {f : α → M} {a : α},
  (a ∈ s → 1 ≤ f a) → 1 ≤ s.mulIndicator f a
-- Mathlib.RingTheory.Finiteness.Basic
/-- See also `Module.Finite.of_surjective` and `LinearMap.finite_iff_of_bijective`.  -/
Module.Finite.of_equiv_equiv : ∀ {A₁ : Type u_6} {B₁ : Type u_7} {A₂ : Type u_8} {B₂ : Type u_9} [inst : CommSemiring A₁] [inst_1 : CommSemiring B₁]
  [inst_2 : CommSemiring A₂] [inst_3 : Semiring B₂] [inst_4 : Algebra A₁ B₁] [inst_5 : Algebra A₂ B₂] (e₁ : A₁ ≃+* A₂)
  (e₂ : B₁ ≃+* B₂),
  (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁) → ∀ [Module.Finite A₁ B₁], Module.Finite A₂ B₂
-- Mathlib.Order.Lattice
/-- Pointwise minimum of two antitone functions is an antitone function.  -/
Antitone.min : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : LinearOrder β] {f g : α → β},
  Antitone f → Antitone g → Antitone fun x => min (f x) (g x)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.single_mul_single : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Mul M] (m₁ m₂ : M) (r₁ r₂ : R),
  MonoidAlgebra.single m₁ r₁ * MonoidAlgebra.single m₂ r₂ = MonoidAlgebra.single (m₁ * m₂) (r₁ * r₂)
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.monoidal_associator_hom_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y Z : CategoryTheory.Comon C),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom.hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        (CategoryTheory.CategoryStruct.id
                (Opposite.op
                  (CategoryTheory.Comon.MonOpOpToComonObj
                      (CategoryTheory.MonoidalCategoryStruct.tensorObj X.ComonToMonOpOpObj
                        Y.ComonToMonOpOpObj)).ComonToMonOpOpObj)).unop.hom.unop
        Z.X)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X.X Y.X Z.X).hom
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X
          (CategoryTheory.CategoryStruct.id
                  (Opposite.op
                    (CategoryTheory.Comon.MonOpOpToComonObj
                        (CategoryTheory.MonoidalCategoryStruct.tensorObj Y.ComonToMonOpOpObj
                          Z.ComonToMonOpOpObj)).ComonToMonOpOpObj)).unop.hom.unop))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_filterMap!_of_getKey?_eq_some : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [Std.TransOrd α] {f : α → β → Option γ} {k k' : α} {fallback : γ},
  t.WF →
    t.getKey? k = some k' →
      Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.filterMap! f t) k fallback =
        ((Std.DTreeMap.Internal.Impl.Const.get? t k).bind fun x => f k' x).getD fallback
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.sdiff_fundamentalInterior : ∀ (G : Type u_1) {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] (s : Set α),
  s \ MeasureTheory.fundamentalInterior G s = MeasureTheory.fundamentalFrontier G s
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.eq_one_iff_unique : ∀ {α : Type u_1}, Cardinal.mk α = 1 ↔ Subsingleton α ∧ Nonempty α
-- Mathlib.Data.Set.NAry
Set.image2_union_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s s' : Set α} {t : Set β},
  Set.image2 f (s ∪ s') t = Set.image2 f s t ∪ Set.image2 f s' t
-- Mathlib.Analysis.InnerProductSpace.Continuous
Dense.eq_zero_of_inner_left : ∀ {E : Type u_4} (𝕜 : Type u_7) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {x : E} {S : Set E}, Dense S → (∀ v ∈ S, inner 𝕜 x v = 0) → x = 0
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than the given key,
returning `fallback` if no such pair exists.
 -/
Std.DTreeMap.Raw.Const.getEntryLTD : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap.Raw α (fun x => β) cmp → α → α × β → α × β
-- Mathlib.CategoryTheory.Sites.MorphismProperty
CategoryTheory.Precoverage.ZeroHypercover.morphismProperty : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {K : CategoryTheory.Precoverage C} {X : C}
  {E : K.ZeroHypercover X} (i : E.I₀), K.morphismProperty (E.f i)
-- Std.Data.DTreeMap.Internal.Cell
/-- Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Cell.getKey? : {α : Type u} → {β : α → Type v} → [inst : Ord α] → {k : α} → Std.DTreeMap.Internal.Cell α β (compare k) → Option α
-- Mathlib.Analysis.Normed.Group.Quotient
NormedAddGroupHom.IsQuotient.surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : SeminormedAddCommGroup M] [inst_1 : SeminormedAddCommGroup N]
  {f : NormedAddGroupHom M N}, f.IsQuotient → Function.Surjective ⇑f
-- Mathlib.RingTheory.PrincipalIdealDomain
Submodule.IsPrincipal.eq_bot_iff_generator_eq_zero : ∀ {R : Type u} {M : Type v} [inst : AddCommMonoid M] [inst_1 : Semiring R] [inst_2 : Module R M] (S : Submodule R M)
  [inst_3 : S.IsPrincipal], S = ⊥ ↔ Submodule.IsPrincipal.generator S = 0
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupNorm.ext : ∀ {E : Type u_3} [inst : Group E] {p q : GroupNorm E}, (∀ (x : E), p x = q x) → p = q
-- Mathlib.Combinatorics.Quiver.Symmetric
Quiver.eq_reverse_iff : ∀ {V : Type u_2} [inst : Quiver V] [h : Quiver.HasInvolutiveReverse V] {a b : V} (f : a ⟶ b) (g : b ⟶ a),
  f = Quiver.reverse g ↔ Quiver.reverse f = g
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.mul_eval : ∀ (l₁ l₂ : Lean.Omega.LinearCombo) (v : Lean.Omega.Coeffs),
  l₁.coeffs.isZero ∨ l₂.coeffs.isZero → (l₁.mul l₂).eval v = l₁.eval v * l₂.eval v
-- Mathlib.RingTheory.Ideal.Height
RingEquiv.height_comap : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] (e : R ≃+* S) (I : Ideal S),
  (Ideal.comap e I).height = I.height
-- Mathlib.NumberTheory.ModularForms.Discriminant
_private.Mathlib.NumberTheory.ModularForms.Discriminant.0.ModularForm.logDeriv_eta_comp_eq_logDeriv_csqrt_eta : ∀ (z : UpperHalfPlane), logDeriv (ModularForm.eta ∘ fun x => -1 / x) ↑z = logDeriv (Complex.sqrt * ModularForm.eta) ↑z
-- Mathlib.Data.Set.Sigma
Set.sigma_subset_preimage_fst : ∀ {ι : Type u_1} {α : ι → Type u_3} (s : Set ι) (t : (i : ι) → Set (α i)), s.sigma t ⊆ Sigma.fst ⁻¹' s
-- Lean.Meta.Tactic.Assert
Lean.Meta.AssertAfterResult : Type
-- Mathlib.Algebra.Category.AlgCat.Limits
AlgCat.forget₂Ring_preservesLimits : ∀ {R : Type u} [inst : CommRing R], CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ (AlgCat R) RingCat)
-- Mathlib.Data.Seq.Parallel
_private.Mathlib.Data.Seq.Parallel.0.Computation.parallel.aux1.match_1.splitter : {α : Type u_1} →
  (motive : Option (Stream'.Seq1 (Option (Computation α))) → Sort u_2) →
    (x : Option (Stream'.Seq1 (Option (Computation α)))) →
      (Unit → motive none) →
        ((S' : Stream'.Seq (Option (Computation α))) → motive (some (none, S'))) →
          ((c : Computation α) → (S' : Stream'.Seq (Option (Computation α))) → motive (some (some c, S'))) → motive x
-- Mathlib.CategoryTheory.Filtered.Small
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsCofiltered.CofilteredClosureSmall.InductiveStep.eq.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {n : ℕ} {X : (k : ℕ) → k < n → (t : Type (max v w)) × (t → C)}
  {k k' : ℕ} {hk : k < n} {hk' : k' < n} {j : (X k hk).fst} {j' : (X k' hk').fst}
  {a a_1 : (X k hk).snd j ⟶ (X k' hk').snd j'} {k_1 k'_1 : ℕ} {hk_1 : k_1 < n} {hk'_1 : k'_1 < n}
  {j_1 : (X k_1 hk_1).fst} {j'_1 : (X k'_1 hk'_1).fst} {a_2 a_3 : (X k_1 hk_1).snd j_1 ⟶ (X k'_1 hk'_1).snd j'_1},
  CategoryTheory.IsCofiltered.CofilteredClosureSmall.InductiveStep.eq✝ hk hk' j j' a a_1 =
      CategoryTheory.IsCofiltered.CofilteredClosureSmall.InductiveStep.eq✝ hk_1 hk'_1 j_1 j'_1 a_2 a_3 →
    k = k_1 ∧ k' = k'_1 ∧ j ≍ j_1 ∧ j' ≍ j'_1 ∧ a ≍ a_2 ∧ a_1 ≍ a_3
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurable_of_le : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι] [SecondCountableTopology ι],
  MeasureTheory.IsStoppingTime f τ → ∀ {i : ι}, (∀ (ω : Ω), τ ω ≤ ↑i) → Measurable τ
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.instReflectsIsomorphismsProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap : (CategoryTheory.forget₂ ProfiniteAddGrp.{u_1} Profinite).ReflectsIsomorphisms
-- Mathlib.CategoryTheory.GlueData
/-- (Implementation) The disjoint union of `U i`.  -/
CategoryTheory.GlueData.sigmaOpens : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v, u₁} C] →
    (D : CategoryTheory.GlueData C) → [CategoryTheory.Limits.HasCoproduct D.U] → C
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
/-- Auxiliary definition for `desc`.  -/
SSet.horn₃₂.desc.multicofork : {X : SSet} →
  (f₀ f₁ f₃ : SSet.stdSimplex.obj { len := 2 } ⟶ X) →
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₁ =
        CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₃ →
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
          CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃ →
        CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₀ =
            CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₁ →
          CategoryTheory.Limits.Multicofork
            ((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map SSet.Subcomplex.toSSetFunctor)
-- Std.Sat.AIG.RefVecOperator.Zip
Std.Sat.AIG.RefVec.zip.go_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {aig : Std.Sat.AIG α} (i : ℕ) (hi : i ≤ len)
  (lhs rhs : aig.RefVec len) (s : aig.RefVec i) (f : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α)
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f] [inst_3 : Std.Sat.AIG.RefVec.LawfulZipOperator α f]
  (idx : ℕ) (h1 : idx < aig.decls.size) (h2 : idx < (Std.Sat.AIG.RefVec.zip.go aig i s hi lhs rhs f).aig.decls.size),
  (Std.Sat.AIG.RefVec.zip.go aig i s hi lhs rhs f).aig.decls[idx] = aig.decls[idx]
-- Mathlib.CategoryTheory.Localization.Construction
/-- The relations by which we take the quotient in order to get the localized category.  -/
CategoryTheory.Localization.Construction.relations : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    (W : CategoryTheory.MorphismProperty C) →
      HomRel (CategoryTheory.Paths (CategoryTheory.Localization.Construction.LocQuiver W))
-- Lean.Elab.App
/-- Create a fresh metavariable for the implicit argument, add it to `f`, and then execute the main loop.
 -/
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.addImplicitArg : Lean.Name → Lean.Elab.Term.ElabAppArgs.M Lean.Expr
-- Init.Data.Array.OfFn
Array.mem_ofFn : ∀ {α : Type u_1} {n : ℕ} {f : Fin n → α} {a : α}, a ∈ Array.ofFn f ↔ ∃ i, f i = a
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.Truncated.sk.full : ∀ (n : ℕ), (SSet.Truncated.sk n).Full