mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Instances
Lean.Meta.Instances.mk.injEq : ∀ (discrTree : Lean.Meta.InstanceTree) (instanceNames : Lean.PHashMap Lean.Name Lean.Meta.InstanceEntry)
  (erased : Lean.PHashSet Lean.Name) (discrTree_1 : Lean.Meta.InstanceTree)
  (instanceNames_1 : Lean.PHashMap Lean.Name Lean.Meta.InstanceEntry) (erased_1 : Lean.PHashSet Lean.Name),
  ({ discrTree := discrTree, instanceNames := instanceNames, erased := erased } =
      { discrTree := discrTree_1, instanceNames := instanceNames_1, erased := erased_1 }) =
    (discrTree = discrTree_1 ∧ instanceNames = instanceNames_1 ∧ erased = erased_1)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
MeasureTheory.eLpNorm_restrict_le : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {ε' : Type u_8} [inst : TopologicalSpace ε'] [inst_1 : ContinuousENorm ε']
  (f : α → ε') (p : ENNReal) (μ : MeasureTheory.Measure α) (s : Set α),
  MeasureTheory.eLpNorm f p (μ.restrict s) ≤ MeasureTheory.eLpNorm f p μ
-- Mathlib.GroupTheory.OrderOfElement
injective_nsmul_iff_not_isOfFinAddOrder : ∀ {G : Type u_1} [inst : AddLeftCancelMonoid G] {x : G}, (Function.Injective fun n => n • x) ↔ ¬IsOfFinAddOrder x
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.conjRingEquiv_symm_apply_apply : ∀ {R₁ : Type u_9} {R₂ : Type u_10} {M₁ : Type u_13} {M₂ : Type u_14} [inst : Semiring R₁] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R₁ M₁] [inst_5 : Module R₂ M₂]
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [inst_6 : RingHomInvPair σ₁₂ σ₂₁] [inst_7 : RingHomInvPair σ₂₁ σ₁₂]
  (e : M₁ ≃ₛₗ[σ₁₂] M₂) (f : M₂ →ₗ[R₂] M₂) (x : M₁), (e.conjRingEquiv.symm f) x = e.symm (f (e x))
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.exists_le_of_tendsto_atBot : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [IsDirectedOrder α] {u : α → β} [inst_2 : Preorder β],
  Filter.Tendsto u Filter.atTop Filter.atBot → ∀ (a : α) (b : β), ∃ a', a ≤ a' ∧ u a' ≤ b
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.GrothendieckTopology.overMapPullback_assoc_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} A] {X Y Z T : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ T)
  {Z_1 : CategoryTheory.Functor (CategoryTheory.Sheaf (J.over T) A) (CategoryTheory.Sheaf (J.over X) A)}
  (h_1 : J.overMapPullback A (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (J.overMapPullbackComp A f (CategoryTheory.CategoryStruct.comp g h)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight (J.overMapPullbackComp A g h).inv (J.overMapPullback A f))
        (CategoryTheory.CategoryStruct.comp
          ((J.overMapPullback A h).associator (J.overMapPullback A g) (J.overMapPullback A f)).hom
          (CategoryTheory.CategoryStruct.comp ((J.overMapPullback A h).whiskerLeft (J.overMapPullbackComp A f g).hom)
            (CategoryTheory.CategoryStruct.comp (J.overMapPullbackComp A (CategoryTheory.CategoryStruct.comp f g) h).hom
              h_1)))) =
    CategoryTheory.CategoryStruct.comp (J.overMapPullbackCongr A ⋯).hom h_1
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.top_add : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, ⊤ + μ = ⊤
-- Mathlib.RingTheory.Ideal.Colon
Submodule.top_colon : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Set M},
  ⊤.colon S = ⊤
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.singleton_mul_singleton : ∀ {α : Type u_2} [inst : Mul α] {a b : α}, {a} * {b} = {a * b}
-- Mathlib.Analysis.Real.OfDigits
Real.hasSum_ofDigitsTerm_digits : ∀ (x : ℝ) {b : ℕ} [inst : NeZero b], 1 < b → x ∈ Set.Ico 0 1 → HasSum (Real.ofDigitsTerm (x.digits b)) x
-- Init.GrindInstances.ToInt
Lean.Grind.instLTInt8SintOfNatNat : Lean.Grind.ToInt.LT Int8 (Lean.Grind.IntInterval.sint 8)
-- Mathlib.CategoryTheory.Monoidal.Closed.Braided
CategoryTheory.ihom.instPreservesLimitsOfShapeOppositeObjFunctorFlipInternalHom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [CategoryTheory.BraidedCategory C] (A : C) [inst_3 : CategoryTheory.MonoidalClosed C] (J : Type u_2)
  [inst_4 : CategoryTheory.Category.{v_2, u_2} J],
  CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.MonoidalClosed.internalHom.flip.obj A)
-- ProofWidgets.Component.HtmlDisplay
ProofWidgets.HtmlDisplayProps.mk : ProofWidgets.Html → ProofWidgets.HtmlDisplayProps
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_diff_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₂ → (t₁ \ t₂)[k]? = t₁[k]?
-- Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
/-- **Eisenstein's lemma**  -/
ZMod.eisenstein_lemma : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)],
  p ≠ 2 → ∀ {a : ℕ}, a % 2 = 1 → ↑a ≠ 0 → legendreSym p ↑a = (-1) ^ ∑ x ∈ Finset.Ico 1 (p / 2).succ, x * a / p
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mkOfOplax'_mapId_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.OplaxFunctor B C) [inst_2 : ∀ (a : B), CategoryTheory.IsIso (F.mapId a)]
  [inst_3 : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.IsIso (F.mapComp f g)] (a : B),
  ((CategoryTheory.Pseudofunctor.mkOfOplax' F).mapId a).inv = CategoryTheory.inv (F.mapId a)
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.LambdaTheoremArgs.id.sizeOf_spec : sizeOf Mathlib.Meta.FunProp.LambdaTheoremArgs.id = 1
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- Eta-expanded form of `CircleIntegrable.add` -/
CircleIntegrable.fun_add : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f g : ℂ → E} {c : ℂ} {R : ℝ},
  CircleIntegrable f c R → CircleIntegrable g c R → CircleIntegrable (fun i => f i + g i) c R
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
AddSubgroup.equivOp_symm_apply_coe : ∀ {G : Type u_2} [inst : AddGroup G] (H : AddSubgroup G) (b : ↥H.op), ↑(H.equivOp.symm b) = AddOpposite.unop ↑b
-- Mathlib.Tactic.Translate.GuessName
/-- Autogenerate additive name.
This runs in several steps:
1) Split according to capitalisation rule and at `_`.
2) Apply word-by-word translation rules.
3) Fix up abbreviations that are not word-by-word translations, like "addComm" or "Nonneg".
 -/
Mathlib.Tactic.GuessName.guessName : Mathlib.Tactic.GuessName.GuessNameData → String → String
-- Mathlib.Data.NNReal.Defs
Set.OrdConnected.preimage_coe_nnreal_real : ∀ {s : Set ℝ}, s.OrdConnected → (NNReal.toReal ⁻¹' s).OrdConnected
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k a : α},
  (m.insert k).get? a = if (k == a) = true ∧ k ∉ m then some k else m.get? a
-- Mathlib.Probability.Density
MeasureTheory.pdf.ofReal_toReal_ae_eq : ∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω}
  {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure ℙ] {X : Ω → E},
  (fun x => ENNReal.ofReal (MeasureTheory.pdf X ℙ μ x).toReal) =ᵐ[μ] MeasureTheory.pdf X ℙ μ
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
/-- An element is in `spinGroup Q` if and only if `star x` is in `spinGroup Q`.
See `star_mem` for only one direction.
 -/
spinGroup.star_mem_iff : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {x : CliffordAlgebra Q}, star x ∈ spinGroup Q ↔ x ∈ spinGroup Q
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec64_div : ∀ {a b : ISize} (h : System.Platform.numBits = 64), (a / b).toBitVec64 h = (a.toBitVec64 h).sdiv (b.toBitVec64 h)
-- Init.Data.UInt.Lemmas
UInt8.ofFin_div : ∀ (a b : Fin UInt8.size), UInt8.ofFin (a / b) = UInt8.ofFin a / UInt8.ofFin b
-- Init.Grind.Order
Lean.Grind.Order.lt_eq_false_of_le : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] {a b : α},
  a ≤ b → (b < a) = False
-- Mathlib.Topology.Continuous
Continuous.closure_preimage_subset : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f → ∀ (t : Set Y), closure (f ⁻¹' t) ⊆ f ⁻¹' closure t
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.subtype.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G),
  H.subtype = { toFun := Subtype.val, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.kernelSequenceE_exact : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₂₃ : j ⟶ l)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.kernelSequenceE_exact._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.kernelSequenceE_exact._auto_3),
  (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).Exact
-- Mathlib.Topology.LocallyFinsupp.Pushforward
Function.locallyFinsupp.support_map_subset_of_forall_mem : ∀ {X : Type u_1} {Y : Type u_2} {R : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}
  (hf : IsSpectralMap f) (w : X → R) [inst_2 : Semiring R] (c : Function.locallyFinsupp X R)
  [inst_3 : PrespectralSpace Y] (s : Set X) (t : Set Y),
  Function.locallyFinsuppWithin.support c ⊆ s →
    (∀ x ∈ s, w x ≠ 0 → f x ∈ t) → Function.locallyFinsuppWithin.support (Function.locallyFinsupp.map f w hf c) ⊆ t
-- Mathlib.Data.Fin.Tuple.Basic
Fin.find_of_not_zero : ∀ {n : ℕ} {p : Fin (n + 1) → Prop} [inst : DecidablePred p] (h : ∃ i, p i) (h0 : ¬p 0),
  Fin.find p h = (Fin.find (fun k => p k.succ) ⋯).succ
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
SSet.Subcomplex.Pairing.WeakRankFunction.isRegular : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {α : Type v} [inst : PartialOrder α] [WellFoundedLT α] [P.IsProper]
  (f : P.WeakRankFunction α), P.IsRegular
-- Mathlib.Algebra.Polynomial.Degree.Support
Polynomial.natDegree_mem_support_of_nonzero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p ≠ 0 → p.natDegree ∈ p.support
-- Mathlib.Data.Set.Function
Set.EqOn.comp_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f : α → β} {g₁ g₂ : β → γ},
  Set.EqOn g₁ g₂ t → Set.MapsTo f s t → Set.EqOn (g₁ ∘ f) (g₂ ∘ f) s
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.leftUnitor_inv_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (X : C)
  {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.SemiCartesianMonoidalCategory.fst (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X) h
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instToJsonCodeActionClientCapabilities.toJson : Lean.Lsp.CodeActionClientCapabilities → Lean.Json
-- Init.Control.Lawful.MonadLift.Instances
ExceptCpsT.instLawfulMonadLiftOfLawfulMonad : ∀ {m : Type u → Type v} {ε : Type u} [inst : Monad m] [LawfulMonad m], LawfulMonadLift m (ExceptCpsT ε m)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.equiv_of_beq : ∀ {α : Type u} {cmp : α → α → Ordering} {m₁ m₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp],
  m₁.WF → m₂.WF → (m₁ == m₂) = true → m₁.Equiv m₂
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.Functor.IsEventuallyConstantFrom.postcomp : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {F : CategoryTheory.Functor J C} {i₀ : J},
  F.IsEventuallyConstantFrom i₀ → ∀ {j : J} (f : i₀ ⟶ j), F.IsEventuallyConstantFrom j
-- Lean.Environment
/-- Returns debug output about the synchronous state of the environment.  -/
Lean.Environment.dbgFormatCheckedSyncState : Lean.Environment → BaseIO String
-- Aesop.RuleSet
/-- The Aesop-specific parts of an Aesop rule set. A `BaseRuleSet` stores global
Aesop rules, e.g. safe and unsafe rules. It does not store simp theorems for
the builtin norm simp rule; these are instead stored in a simp extension.
 -/
Aesop.BaseRuleSet : Type
-- Init.Data.UInt.Lemmas
UInt8.right_eq_add : ∀ {a b : UInt8}, b = a + b ↔ a = 0
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.kernel_sum_seq : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β)
  [h : ProbabilityTheory.IsSFiniteKernel κ], ProbabilityTheory.Kernel.sum κ.seq = κ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.hom_ext_iff : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂}
  {sq : F.PushoutObjObj f₁ f₂} {X₃ : C₃} {f g : sq.pt ⟶ X₃},
  f = g ↔
    CategoryTheory.CategoryStruct.comp sq.inl f = CategoryTheory.CategoryStruct.comp sq.inl g ∧
      CategoryTheory.CategoryStruct.comp sq.inr f = CategoryTheory.CategoryStruct.comp sq.inr g
-- Mathlib.Algebra.Order.Module.HahnEmbedding
LinearPMap.supSpanSingleton.congr_simp : ∀ {E : Type u_4} [inst : AddCommGroup E] {F : Type u_5} [inst_1 : AddCommGroup F] {K : Type u_7} {L : Type u_8}
  [inst_2 : DivisionRing K] [inst_3 : DivisionRing L] {σ : K →+* L} [inst_4 : Module K E] [inst_5 : Module L F]
  (f f_1 : E →ₛₗ.[σ] F) (e_f : f = f_1) (x x_1 : E) (e_x : x = x_1) (y y_1 : F),
  y = y_1 → ∀ (hx : x ∉ f.domain), f.supSpanSingleton x y hx = f_1.supSpanSingleton x_1 y_1 ⋯
-- Mathlib.CategoryTheory.Localization.Bifunctor
CategoryTheory.Localization.lift₂NatIso_inv : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} {E : Type u_5}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} E] (L₁ : CategoryTheory.Functor C₁ D₁)
  (L₂ : CategoryTheory.Functor C₂ D₂) (W₁ : CategoryTheory.MorphismProperty C₁)
  (W₂ : CategoryTheory.MorphismProperty C₂) [inst_5 : L₁.IsLocalization W₁] [inst_6 : L₂.IsLocalization W₂]
  [inst_7 : W₁.ContainsIdentities] [inst_8 : W₂.ContainsIdentities]
  (F₁ F₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E))
  (F₁' F₂' : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E))
  [inst_9 : CategoryTheory.Localization.Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁']
  [inst_10 : CategoryTheory.Localization.Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'] (e : F₁ ≅ F₂),
  (CategoryTheory.Localization.lift₂NatIso L₁ L₂ W₁ W₂ F₁ F₂ F₁' F₂' e).inv =
    CategoryTheory.Localization.lift₂NatTrans L₁ L₂ W₁ W₂ F₂ F₁ F₂' F₁' e.inv
-- Lean.Elab.App
Lean.Elab.Term.instInhabitedElabElimInfo : Inhabited Lean.Elab.Term.ElabElimInfo
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.setTag.inj : ∀ {x : Lean.IR.VarId} {cidx : ℕ} {b : Lean.IR.FnBody} {x_1 : Lean.IR.VarId} {cidx_1 : ℕ} {b_1 : Lean.IR.FnBody},
  Lean.IR.FnBody.setTag x cidx b = Lean.IR.FnBody.setTag x_1 cidx_1 b_1 → x = x_1 ∧ cidx = cidx_1 ∧ b = b_1
-- Mathlib.Computability.Encoding
Computability.decode_encodePosNum : ∀ (n : PosNum), Computability.decodePosNum (Computability.encodePosNum n) = n
-- Mathlib.Analysis.InnerProductSpace.NormDet
LinearMap.normDet_zero : ∀ {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup U]
  [inst_2 : InnerProductSpace 𝕜 U] [inst_3 : FiniteDimensional 𝕜 U] [inst_4 : NormedAddCommGroup V]
  [inst_5 : InnerProductSpace 𝕜 V], LinearMap.normDet 0 = 0 ^ Module.finrank 𝕜 U
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.coreS.inj : ∀ {a b : Lean.Expr} {sa sb : Lean.Meta.Grind.Arith.CommRing.SemiringExpr}
  {ra rb : Lean.Meta.Grind.Arith.CommRing.RingExpr} {a_1 b_1 : Lean.Expr}
  {sa_1 sb_1 : Lean.Meta.Grind.Arith.CommRing.SemiringExpr} {ra_1 rb_1 : Lean.Meta.Grind.Arith.CommRing.RingExpr},
  Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.coreS a b sa sb ra rb =
      Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.coreS a_1 b_1 sa_1 sb_1 ra_1 rb_1 →
    a = a_1 ∧ b = b_1 ∧ sa = sa_1 ∧ sb = sb_1 ∧ ra = ra_1 ∧ rb = rb_1
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.map_η_comp_η : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [e.IsMonoidal],
  CategoryTheory.CategoryStruct.comp (e.functor.map (CategoryTheory.Functor.OplaxMonoidal.η e.inverse))
      (CategoryTheory.Functor.OplaxMonoidal.η e.functor) =
    e.counit.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)
-- Mathlib.RingTheory.Flat.Basic
/-- Tensor product of linearly independent families is linearly
independent under some flatness conditions.

The flatness condition could be removed over domains.
See `LinearIndependent.tmul_of_isDomain`.  -/
LinearIndependent.tmul_of_flat_left : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} {N : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {ι : Type u_6} {κ : Type u_7} {v : ι → M}
  {w : κ → N} [Module.Flat R M],
  LinearIndependent R v → LinearIndependent R w → LinearIndependent R fun i => v i.1 ⊗ₜ[R] w i.2
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_emptyWithCapacity : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {a : α} {c : ℕ}, (Std.HashMap.emptyWithCapacity c)[a]? = none
-- Mathlib.RingTheory.Congruence.Hom
RingCon.rangeS_mk' : ∀ {M : Type u_1} [inst : NonAssocSemiring M] {c : RingCon M}, c.mk'.rangeS = ⊤
-- Mathlib.Order.Preorder.Chain
Flag.instSetLike : {α : Type u_1} → [inst : LE α] → SetLike (Flag α) α
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
/-- The arrows pseudo-equal to a zero morphism are precisely the zero morphisms.  -/
CategoryTheory.Abelian.Pseudoelement.pseudoZero_aux : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P : C} (Q : C)
  (f : CategoryTheory.Over P), f ≈ CategoryTheory.Over.mk 0 ↔ f.hom = 0
-- Mathlib.Analysis.Normed.Group.Basic
norm_sum_le_of_le : ∀ {ι : Type u_3} {E : Type u_5} [inst : SeminormedAddCommGroup E] (s : Finset ι) {f : ι → E} {n : ι → ℝ},
  (∀ b ∈ s, ‖f b‖ ≤ n b) → ‖∑ b ∈ s, f b‖ ≤ ∑ b ∈ s, n b
-- Lean.Data.Lsp.Basic
Lean.Lsp.DocumentFilter.pattern? : Lean.Lsp.DocumentFilter → Option String
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getKeyGE_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α} {h' : ∃ a ∈ t₁, (cmp a k).isGE = true} (h : t₁.Equiv t₂), t₁.getKeyGE k h' = t₂.getKeyGE k ⋯
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.instInhabitedTrie.default : {α : Type} → Lean.Meta.LazyDiscrTree.Trie α
-- Mathlib.Order.Hom.WithTopBot
LatticeHom.withBotWithTop_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst_1 : Lattice β] (f : LatticeHom α β) (a : WithBot (WithTop α)),
  f.withBotWithTop a = WithBot.map (WithTop.map ⇑f) a
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isRetrocompact_zeroLocus_compl_of_fg : ∀ {R : Type u} [inst : CommSemiring R] {I : Ideal R}, I.FG → IsRetrocompact (PrimeSpectrum.zeroLocus ↑I)ᶜ
-- Lean.DocString.Markdown
Lean.Doc.instMarkdownInlineEmpty : Lean.Doc.MarkdownInline Empty
-- Std.Http.Protocol.H1.Reader
/-- Paused waiting for a `canContinue` decision, carrying the next state.
 -/
Std.Http.Protocol.H1.Reader.State.continue : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Reader.State dir → Std.Http.Protocol.H1.Reader.State dir
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.precompR_apply : ∀ {𝕜 : Type u_1} {E : Type u_4} (Eₗ : Type u_5) {Fₗ : Type u_7} {Gₗ : Type u_9} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup Eₗ] [inst_2 : SeminormedAddCommGroup Fₗ] [inst_3 : SeminormedAddCommGroup Gₗ]
  [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 E] [inst_6 : NormedSpace 𝕜 Eₗ]
  [inst_7 : NormedSpace 𝕜 Fₗ] [inst_8 : NormedSpace 𝕜 Gₗ] (L : E →L[𝕜] Fₗ →L[𝕜] Gₗ) (x : E),
  (ContinuousLinearMap.precompR Eₗ L) x = (ContinuousLinearMap.compL 𝕜 Eₗ Fₗ Gₗ) (L x)
-- Init.Data.Fin.Lemmas
Fin.natAdd_eq_addNat : ∀ (n : ℕ) (i : Fin n), Fin.natAdd n i = i.addNat n
-- Init.Data.Array.MinMax
Array.max?_empty : ∀ {α : Type u_1} [inst : Max α], #[].max? = none
-- Mathlib.AlgebraicGeometry.Geometrically.Basic
AlgebraicGeometry.fiber_of_geometrically : ∀ {P : CategoryTheory.ObjectProperty AlgebraicGeometry.Scheme} {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  AlgebraicGeometry.geometrically P f → ∀ (y : ↥Y), P (AlgebraicGeometry.Scheme.Hom.fiber f y)
-- Mathlib.Data.ENat.Basic
instCanonicallyOrderedAddENat : CanonicallyOrderedAdd ℕ∞
-- Mathlib.RingTheory.RegularLocalRing.Defs
IsRegularLocalRing.toIsLocalRing : ∀ {R : Type u_1} {inst : CommRing R} [self : IsRegularLocalRing R], IsLocalRing R
-- Mathlib.GroupTheory.FinitelyPresentedGroup
AddGroup.IsFinitelyPresented.out : ∀ {G : Type u_5} {inst : AddGroup G} [self : AddGroup.IsFinitelyPresented G],
  ∃ n φ, Function.Surjective ⇑φ ∧ φ.ker.IsFinitelyNormallyGenerated
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
constFormalMultilinearSeries_zero : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F],
  constFormalMultilinearSeries 𝕜 E 0 = 0
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.basis.eq_1 : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] (s : Finset ι) (v : ι → F) (i : ι),
  Lagrange.basis s v i = ∏ j ∈ s.erase i, Lagrange.basisDivisor (v i) (v j)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.bot_parallel_iff_eq_bot : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : AffineSubspace k P}, ⊥.Parallel s ↔ s = ⊥
-- Mathlib.Data.Finset.Insert
Finset.singleton_ne_empty : ∀ {α : Type u_1} (a : α), {a} ≠ ∅
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
/-- The morphism `K.truncLE n ⟶ L.truncLE n` induced by a morphism `K ⟶ L`.  -/
CochainComplex.truncLEMap : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {K L : CochainComplex C ℤ} →
        (K ⟶ L) →
          [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
            [inst_3 : ∀ (i : ℤ), HomologicalComplex.HasHomology K i] →
              [inst_4 : ∀ (i : ℤ), HomologicalComplex.HasHomology L i] → (n : ℤ) → K.truncLE n ⟶ L.truncLE n
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.mk.sizeOf_spec : ∀ {R : Type u} [inst : Ring R] [inst_1 : TopologicalSpace R] [inst_2 : SizeOf R] (toModuleCat : ModuleCat R)
  [topologicalSpace : TopologicalSpace ↑toModuleCat] [isTopologicalAddGroup : IsTopologicalAddGroup ↑toModuleCat]
  [continuousSMul : ContinuousSMul R ↑toModuleCat],
  sizeOf
      { toModuleCat := toModuleCat, topologicalSpace := topologicalSpace,
        isTopologicalAddGroup := isTopologicalAddGroup, continuousSMul := continuousSMul } =
    1 + sizeOf toModuleCat + sizeOf topologicalSpace + sizeOf isTopologicalAddGroup + sizeOf continuousSMul