mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Etale.Finite
Algebra.FormallyEtale.equivPiOfIsSepClosed.congr_simp : ∀ (K : Type u_1) (A : Type u) [inst : Field K] [inst_1 : CommRing A] [inst_2 : Algebra K A]
  [inst_3 : Algebra.EssFiniteType K A] [inst_4 : Algebra.FormallyEtale K A] [inst_5 : IsSepClosed K],
  Algebra.FormallyEtale.equivPiOfIsSepClosed K A = Algebra.FormallyEtale.equivPiOfIsSepClosed K A
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.negAddY_neg : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} {P : Fin 3 → R},
  W'.Equation P → W'.negAddY P (W'.neg P) = W'.dblZ P
-- Lean.Meta.Tactic.Contradiction
/-- Return `true` if goal `mvarId` has contradictory hypotheses.
See `MVarId.contradiction` for the list of tests performed by this method.
 -/
Lean.MVarId.contradictionCore : Lean.MVarId → Lean.Meta.Contradiction.Config → Lean.MetaM Bool
-- Lean.Parser.Syntax
Lean.Parser.Command.catBehavior.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.comap_map_eq_self : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {p : Submodule R M},
  f.ker ≤ p → Submodule.comap f (Submodule.map f p) = p
-- Init.Data.Nat.Lemmas
Nat.lt_mul_div_succ : ∀ {b : ℕ} (a : ℕ), 0 < b → a < b * (a / b + 1)
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (hom : X ⟶ Y) →
        (inv : Y ⟶ X) →
          autoParam (CategoryTheory.CategoryStruct.comp hom inv = CategoryTheory.CategoryStruct.id X)
              CategoryTheory.Iso.hom_inv_id._autoParam →
            autoParam (CategoryTheory.CategoryStruct.comp inv hom = CategoryTheory.CategoryStruct.id Y)
                CategoryTheory.Iso.inv_hom_id._autoParam →
              (X ≅ Y)
-- Mathlib.Algebra.Ring.CharZero
nat_mul_inj' : ∀ {R : Type u_2} [inst : NonAssocRing R] [NoZeroDivisors R] [CharZero R] {n : ℕ} {a b : R},
  ↑n * a = ↑n * b → n ≠ 0 → a = b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] {k k' : α}
  {v : β},
  t.WF →
    (List.find? (fun a => compare a.1 k == Ordering.eq) (Std.DTreeMap.Internal.Impl.Const.toList t) = some (k', v) ↔
      t.getKey? k = some k' ∧ Std.DTreeMap.Internal.Impl.Const.get? t k = some v)
-- Aesop.Rule.Name
Aesop.BuilderName.destruct.sizeOf_spec : sizeOf Aesop.BuilderName.destruct = 1
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- The Jacobi symbol is multiplicative in its first argument.  -/
jacobiSym.mul_left : ∀ (a₁ a₂ : ℤ) (b : ℕ), jacobiSym (a₁ * a₂) b = jacobiSym a₁ b * jacobiSym a₂ b
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instInhabitedCompletionItemKind.default : Lean.Lsp.CompletionItemKind
-- Mathlib.LinearAlgebra.Alternating.DomCoprod
AlternatingMap.domCoprod.summand.eq_1 : ∀ {ιa : Type u_1} {ιb : Type u_2} [inst : Fintype ιa] [inst_1 : Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4}
  {N₁ : Type u_5} {N₂ : Type u_6} [inst_2 : CommSemiring R'] [inst_3 : AddCommGroup N₁] [inst_4 : Module R' N₁]
  [inst_5 : AddCommGroup N₂] [inst_6 : Module R' N₂] [inst_7 : AddCommMonoid Mᵢ] [inst_8 : Module R' Mᵢ]
  [inst_9 : DecidableEq ιa] [inst_10 : DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂)
  (σ : Equiv.Perm.ModSumCongr ιa ιb),
  AlternatingMap.domCoprod.summand a b σ =
    Quotient.liftOn' σ (fun σ => Equiv.Perm.sign σ • MultilinearMap.domDomCongr σ ((↑a).domCoprod ↑b)) ⋯
-- Mathlib.Analysis.Normed.Operator.Basic
ball_zero_subset_range_iff_surjective : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} {𝓕 : Type u_8} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : FunLike 𝓕 E F]
  [SemilinearMapClass 𝓕 σ₁₂ E F] [RingHomSurjective σ₁₂] {f : 𝓕} {r : ℝ},
  0 < r → (Metric.ball 0 r ⊆ Set.range ⇑f ↔ Function.Surjective ⇑f)
-- Mathlib.CategoryTheory.Category.Cat.Terminal
CategoryTheory.Cat.instHasTerminal : CategoryTheory.Limits.HasTerminal CategoryTheory.Cat
-- Mathlib.MeasureTheory.Function.EssSup
essSup_count : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : CompleteLattice β] [MeasurableSingletonClass α]
  (f : α → β), essSup f MeasureTheory.Measure.count = ⨆ i, f i
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
/-- The inclusion functor `BifibrantObject C ⥤ C`.  -/
HomotopicalAlgebra.BifibrantObject.ι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C] →
      [inst_2 : CategoryTheory.Limits.HasInitial C] →
        [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C] →
          [inst_4 : CategoryTheory.Limits.HasTerminal C] →
            CategoryTheory.Functor (HomotopicalAlgebra.BifibrantObject C) C
-- Mathlib.Algebra.Group.Action.Defs
smul_smul_smul_comm : ∀ {α : Type u_5} {β : Type u_6} {γ : Type u_7} {δ : Type u_8} [inst : SMul α β] [inst_1 : SMul α γ] [inst_2 : SMul β δ]
  [inst_3 : SMul α δ] [inst_4 : SMul γ δ] [IsScalarTower α β δ] [IsScalarTower α γ δ] [SMulCommClass β γ δ] (a : α)
  (b : β) (c : γ) (d : δ), (a • b) • c • d = (a • c) • b • d
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- Derivative of `f` at the point `x`, if it exists.  Zero otherwise.

If the derivative exists (i.e., `∃ f', HasDerivAt f f' x`), then
`f x' = f x + (x' - x) • deriv f x + o(x' - x)` where `x'` converges to `x`.
 -/
deriv : {𝕜 : Type u} →
  [inst : NontriviallyNormedField 𝕜] →
    {F : Type v} → [inst_1 : AddCommGroup F] → [Module 𝕜 F] → [TopologicalSpace F] → (𝕜 → F) → 𝕜 → F
-- Mathlib.Data.TypeVec
/-- `prod` is functorial  -/
MvFunctor.«term_⊗'_» : Lean.TrailingParserDescr
-- Init.Grind.FieldNormNum
Lean.Grind.Field.NormNum.intCast_eq : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] (n : ℤ), IntCast.intCast n = Lean.Grind.Field.NormNum.ofRat ↑n
-- Mathlib.Tactic.Positivity.Core
/-- Extract a proof that `e` is nonzero, if possible, from `Strictness` information about `e`.  -/
Mathlib.Meta.Positivity.Strictness.toNonzero : {u : Lean.Level} →
  {α : Q(Type u)} →
    (zα : Q(Zero «$α»)) →
      {e : Q(«$α»)} →
        {pα? : Option Q(PartialOrder «$α»)} → Mathlib.Meta.Positivity.Strictness zα e pα? → Option Q(«$e» ≠ 0)
-- Mathlib.Data.List.Rotate
List.IsRotated.mem_iff : ∀ {α : Type u} {l l' : List α}, l ~r l' → ∀ {a : α}, a ∈ l ↔ a ∈ l'
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.comap_comap : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {P : Type u_6} [inst_2 : AddGroup P]
  (K : AddSubgroup P) (g : N →+ P) (f : G →+ N),
  AddSubgroup.comap f (AddSubgroup.comap g K) = AddSubgroup.comap (g.comp f) K
-- Aesop.Search.Expansion
_private.Aesop.Search.Expansion.0.Aesop.expandGoal.fmtNorm : {Q : Type} → [inst : Aesop.Queue Q] → Except Lean.Exception Bool → Aesop.SearchM Q Lean.MessageData
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_insertIfNew_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, k ∈ t.insertIfNew k v
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
List.formPerm_disjoint_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {l l' : List α},
  l.Nodup → l'.Nodup → 2 ≤ l.length → 2 ≤ l'.length → (l.formPerm.Disjoint l'.formPerm ↔ l.Disjoint l')
-- Mathlib.Combinatorics.Configuration
Configuration.HasPoints.toNondegenerate : ∀ {P : Type u_1} {L : Type u_2} {inst : Membership P L} [self : Configuration.HasPoints P L],
  Configuration.Nondegenerate P L
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitArg.arg : Lean.Meta.Grind.SplitArg → Lean.Expr
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.az.eq_1 : ∀ (a : ℕ), Pell.az a = ↑a
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.FullyFaithful.whiskeringRight_preimage_app : ∀ {D : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} E]
  {F : CategoryTheory.Functor D E} (hF : F.FullyFaithful) (C : Type u_1) [inst_2 : CategoryTheory.Category.{v_1, u_1} C]
  {X Y : CategoryTheory.Functor C D}
  (f :
    ((CategoryTheory.Functor.whiskeringRight C D E).obj F).obj X ⟶
      ((CategoryTheory.Functor.whiskeringRight C D E).obj F).obj Y)
  (X_1 : C), ((hF.whiskeringRight C).preimage f).app X_1 = hF.preimage (f.app X_1)
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.rTensor_zero : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P], LinearMap.rTensor M 0 = 0
-- Mathlib.Algebra.Order.Interval.Basic
instDivNonemptyInterval : {α : Type u_2} → [inst : Preorder α] → [inst_1 : CommGroup α] → [MulLeftMono α] → Div (NonemptyInterval α)
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
/-- The object.  -/
CategoryTheory.PreZeroHypercover.Relation.obj : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {S : C} → {E : CategoryTheory.PreZeroHypercover S} → {i j : E.I₀} → E.Relation i j → C
-- Mathlib.GroupTheory.OrderOfElement
Subgroup.orderOf_dvd_natCard : ∀ {G : Type u_6} [inst : Group G] (s : Subgroup G) {x : G}, x ∈ s → orderOf x ∣ Nat.card ↥s
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.setToL1_congr_left : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : CompleteSpace F] (T T' : Set α → E →L[ℝ] F) {C C' : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C'),
  T = T' → ∀ (f : ↥(MeasureTheory.Lp E 1 μ)), (MeasureTheory.L1.setToL1 hT) f = (MeasureTheory.L1.setToL1 hT') f
-- Mathlib.Topology.ClusterPt
/-- **Alias** of the forward direction of `mapClusterPt_def`. -/
MapClusterPt.clusterPt : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {F : Filter α} {u : α → X} {x : X},
  MapClusterPt x F u → ClusterPt x (Filter.map u F)
-- Mathlib.Tactic.Simps.Basic
Simps.instToMessageDataProjectionRule : Lean.ToMessageData Simps.ProjectionRule
-- Mathlib.Algebra.Order.UpperLower
LowerSet.coe_sub : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedAddMonoid α] (s t : LowerSet α),
  ↑(s - t) = ↑s - ↑t
-- Mathlib.Computability.TuringMachine.Tape
Turing.BlankExtends.trans : ∀ {Γ : Type u_1} [inst : Inhabited Γ] {l₁ l₂ l₃ : List Γ},
  Turing.BlankExtends l₁ l₂ → Turing.BlankExtends l₂ l₃ → Turing.BlankExtends l₁ l₃
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
/-- An infinite place is not unramified (i.e. ramified) iff it is a complex place above a real place.
 -/
NumberField.InfinitePlace.not_isUnramified_iff : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K]
  {w : NumberField.InfinitePlace K},
  ¬NumberField.InfinitePlace.IsUnramified k w ↔ w.IsComplex ∧ (w.comap (algebraMap k K)).IsReal
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.modify.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.LawfulEqCmp cmp] (t t_1 : Std.DTreeMap α β cmp),
  t = t_1 → ∀ (a : α) (f f_1 : β a → β a), f = f_1 → t.modify a f = t_1.modify a f_1
-- Mathlib.Control.Random
Random.instBoundedRandomULiftOfULiftableOfMonad : {m : Type u → Type u_1} →
  {m' : Type (max v u) → Type u_2} →
    {α : Type u} →
      [inst : Preorder α] → [ULiftable m m'] → [BoundedRandom m α] → [Monad m'] → BoundedRandom m' (ULift.{v, u} α)
-- Aesop.Search.Expansion
Aesop.RuleResult.succeeded.inj : ∀ {newRapps newRapps_1 : Array Aesop.RappRef},
  Aesop.RuleResult.succeeded newRapps = Aesop.RuleResult.succeeded newRapps_1 → newRapps = newRapps_1
-- Mathlib.Topology.Algebra.Group.GroupTopology
/-- A version of the global `continuous_inv` suitable for dot notation.  -/
GroupTopology.continuous_inv' : ∀ {α : Type u} [inst : Group α] (g : GroupTopology α), Continuous Inv.inv
-- Init.Data.Float.Model.Unpacked.Operations.OfNat
/-- Converts a `USize` to an `UnpackedFloat`, returning positive zero on zero.  -/
Float.Model.UnpackedFloat.ofUSize : Float.Model.Format → USize → Float.Model.UnpackedFloat
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.f_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (self : CategoryTheory.GlueData C) (i : self.J),
  CategoryTheory.IsIso (self.f i i)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- A function `f : G × G → A` satisfies the 2-cocycle condition if
`f(gh, j) + f(g, h) = g • f(h, j) + f(g, hj)` for all `g, h : G`.  -/
groupCohomology.IsCocycle₂ : {G : Type u_1} → {A : Type u_2} → [Mul G] → [AddCommGroup A] → [SMul G A] → (G × G → A) → Prop
-- Lean.Meta.Tactic.SplitIf
_private.Lean.Meta.Tactic.SplitIf.0.Lean.Meta.findSplit?.find?.unsafe_impl_2 : Lean.Meta.SplitKind → Lean.ExprSet → Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.AssocList.foldlM.match_1.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} {δ : Type u_4} (motive : δ → Std.DHashMap.Internal.AssocList α β → Sort u_3) (d : δ)
  (h_1 : (d : δ) → motive d Std.DHashMap.Internal.AssocList.nil)
  (h_2 :
    (d : δ) →
      (a : α) →
        (b : β a) →
          (es : Std.DHashMap.Internal.AssocList α β) → motive d (Std.DHashMap.Internal.AssocList.cons a b es)),
  (match d, Std.DHashMap.Internal.AssocList.nil with
    | d, Std.DHashMap.Internal.AssocList.nil => h_1 d
    | d, Std.DHashMap.Internal.AssocList.cons a b es => h_2 d a b es) =
    h_1 d
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
CategoryTheory.Functor.LaxMonoidal.whiskeringRight_μ_app : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.MonoidalCategory D] [inst_4 : CategoryTheory.MonoidalCategory E]
  (L : CategoryTheory.Functor D E) [inst_5 : L.LaxMonoidal] (F G : CategoryTheory.Functor C D) (X : C),
  (CategoryTheory.Functor.LaxMonoidal.μ ((CategoryTheory.Functor.whiskeringRight C D E).obj L) F G).app X =
    CategoryTheory.Functor.LaxMonoidal.μ L (F.obj X) (G.obj X)
-- Mathlib.Algebra.Group.Subgroup.Finite
Fintype.card_coeSort_range : ∀ {G : Type u_1} [inst : Group G] {N : Type u_3} [inst_1 : Group N] [inst_2 : Fintype G] [inst_3 : DecidableEq N]
  {f : G →* N}, Function.Injective ⇑f → Fintype.card ↥f.range = Fintype.card G
-- Init.Data.List.Lemmas
List.sum_reverse : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : Add α] [Std.Associative fun x1 x2 => x1 + x2]
  [Std.Commutative fun x1 x2 => x1 + x2] [Std.LawfulLeftIdentity (fun x1 x2 => x1 + x2) 0] (xs : List α),
  xs.reverse.sum = xs.sum
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.addCommSemigroup.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst_1 : AddCommSemigroup M₂] (f : M₁ → M₂)
  (hf : Function.Injective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y),
  Function.Injective.addCommSemigroup f hf mul =
    { toAddSemigroup := Function.Injective.addSemigroup f hf mul, add_comm := ⋯ }
-- Mathlib.Topology.Algebra.InfiniteSum.Group
tsum_neg : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α]
  [IsTopologicalAddGroup α] {f : β → α} [T2Space α], ∑'[L] (b : β), -f b = -∑'[L] (b : β), f b
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- The quotient map from the 2-cocycles of `A`, as a submodule of `G × G → A`, to `H²(G, A)`.  -/
groupCohomology.H2π : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → (A : Rep.{u, u, u} k G) → ModuleCat.of k ↥(groupCohomology.cocycles₂ A) ⟶ groupCohomology.H2 A
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.assignUnassignedLevelMVars.search : Lean.Expr →
  Lean.Expr →
    Array (Lean.Expr × Array Lean.Expr) →
      Array Lean.Level → ℕ → StateRefT' IO.RealWorld (Array (Lean.Expr × Lean.Expr)) Lean.MetaM Unit
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.DecreasingBy.mk.inj : ∀ {ref : Lean.Syntax} {tactic : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq} {ref_1 : Lean.Syntax}
  {tactic_1 : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq},
  { ref := ref, tactic := tactic } = { ref := ref_1, tactic := tactic_1 } → ref = ref_1 ∧ tactic = tactic_1
-- Mathlib.MeasureTheory.Measure.OpenPos
IsOpen.ae_eq_empty_iff_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure]
  {U : Set X}, IsOpen U → (U =ᵐ[μ] ∅ ↔ U = ∅)
-- Mathlib.Logic.Relation
/-- The composition of two relations, yielding a new relation.  The result
relates a term of `α` and a term of `γ` if there is an intermediate
term of `β` related to both.
 -/
Relation.Comp : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (α → β → Prop) → (β → γ → Prop) → α → γ → Prop
-- Mathlib.Analysis.Normed.Group.Defs
/-- Construct a seminormed group from a translation-invariant pseudodistance.  -/
SeminormedAddGroup.ofAddDist' : {E : Type u_5} →
  [inst : Norm E] →
    [inst_1 : AddGroup E] →
      [inst_2 : PseudoMetricSpace E] →
        (∀ (x : E), ‖x‖ = dist 0 x) → (∀ (x y z : E), dist (z + x) (z + y) ≤ dist x y) → SeminormedAddGroup E
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.residue_ne_zero_iff_isUnit : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R] (x : R), (IsLocalRing.residue R) x ≠ 0 ↔ IsUnit x
-- Lean.Level
/-- Auxiliary function used at `normalize`  -/
_private.Lean.Level.0.Lean.Level.getMaxArgsAux : (Lean.Level → Lean.Level) → Lean.Level → Bool → Array Lean.Level → Array Lean.Level
-- Lean.Elab.Term.TermElabM
/-- Tactic metavariable arising from an autoparam for a function application.  -/
Lean.Elab.Term.TacticMVarKind.autoParam : Lean.Name → Lean.Elab.Term.TacticMVarKind
-- Mathlib.Order.Lattice
Prod.swap_inf : ∀ (α : Type u) (β : Type v) [inst : Min α] [inst_1 : Min β] (p q : α × β), (p ⊓ q).swap = p.swap ⊓ q.swap
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
/-- If bounded continuous functions tend to the indicator of a measurable set and are
uniformly bounded, then their integrals against a finite measure tend to the measure of the set.
This formulation assumes:
* the functions tend to a limit along a countably generated filter;
* the limit is in the almost everywhere sense;
* boundedness holds almost everywhere.
 -/
MeasureTheory.measure_of_cont_bdd_of_tendsto_filter_indicator : ∀ {Ω : Type u_1} [inst : TopologicalSpace Ω] [inst_1 : MeasurableSpace Ω] [OpensMeasurableSpace Ω] {ι : Type u_2}
  {L : Filter ι} [L.IsCountablyGenerated] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] {c : NNReal}
  {E : Set Ω},
  MeasurableSet E →
    ∀ (fs : ι → BoundedContinuousFunction Ω NNReal),
      (∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c) →
        (∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun i => (fs i) ω) L (nhds (E.indicator (fun x => 1) ω))) →
          Filter.Tendsto (fun n => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂μ) L (nhds (μ E))
-- Aesop.Saturate
Aesop.SaturateM.Context.mk.inj : ∀ {options options_1 : Aesop.Options'}, { options := options } = { options := options_1 } → options = options_1
-- Mathlib.Algebra.Module.Torsion.Basic
/-- The torsion submodule, containing all elements `x` of `M` such that `a • x = 0` for some
non-zero-divisor `a` in `R`.  -/
Submodule.torsion : (R : Type u_1) →
  (M : Type u_2) → [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Submodule R M
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse_obj_left_as : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T × T)
  (Y : CategoryTheory.StructuredArrow X.2 (CategoryTheory.Under.forget X.1)),
  ((CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse X).obj Y).left.as = PUnit.unit
-- Mathlib.RingTheory.PowerSeries.WellKnown
PowerSeries.invOneSubPow_val_eq_mk_sub_one_add_choose_of_pos : ∀ (S : Type u_1) [inst : CommRing S] (d : ℕ),
  0 < d → ↑(PowerSeries.invOneSubPow S d) = PowerSeries.mk fun n => ↑((d - 1 + n).choose (d - 1))
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.comp.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y Z : C} {a b : ℕ} (α α_1 : CategoryTheory.Abelian.Ext X Y a),
  α = α_1 →
    ∀ (β β_1 : CategoryTheory.Abelian.Ext Y Z b), β = β_1 → ∀ {c : ℕ} (h : a + b = c), α.comp β h = α_1.comp β_1 h
-- Mathlib.Order.SuccPred.Tree
/-- The type should be a `SemilatticeInf`,
where `inf` is the least common ancestor in the tree.  -/
RootedTree.semilatticeInf : (self : RootedTree) → SemilatticeInf ↑self
-- Mathlib.ModelTheory.Syntax
/-- Maps a term's symbols along a language map.  -/
FirstOrder.Language.LHom.onTerm : {L : FirstOrder.Language} → {L' : FirstOrder.Language} → {α : Type u'} → (L →ᴸ L') → L.Term α → L'.Term α
-- Mathlib.Analysis.MeanInequalitiesPow
Real.rpow_arith_mean_le_arith_mean_rpow : ∀ {ι : Type u} (s : Finset ι) (w z : ι → ℝ),
  (∀ i ∈ s, 0 ≤ w i) →
    ∑ i ∈ s, w i = 1 → (∀ i ∈ s, 0 ≤ z i) → ∀ {p : ℝ}, 1 ≤ p → (∑ i ∈ s, w i * z i) ^ p ≤ ∑ i ∈ s, w i * z i ^ p
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.Integrable.integral_prod_right : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  [inst_4 : NormedSpace ℝ E] [MeasureTheory.SFinite μ] ⦃f : α × β → E⦄,
  MeasureTheory.Integrable f (μ.prod ν) → MeasureTheory.Integrable (fun y => ∫ (x : α), f (x, y) ∂μ) ν
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.brecOn.go : {motive_1 : Lean.IR.Alt → Sort u} →
  {motive_2 : Lean.IR.FnBody → Sort u} →
    {motive_3 : Array Lean.IR.Alt → Sort u} →
      {motive_4 : List Lean.IR.Alt → Sort u} →
        (t : Lean.IR.FnBody) →
          ((t : Lean.IR.Alt) → t.below → motive_1 t) →
            ((t : Lean.IR.FnBody) → t.below → motive_2 t) →
              ((t : Array Lean.IR.Alt) → Lean.IR.Alt.below_1 t → motive_3 t) →
                ((t : List Lean.IR.Alt) → Lean.IR.Alt.below_2 t → motive_4 t) → motive_2 t ×' t.below
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.characteristic_iff_le_map : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.Characteristic ↔ ∀ (ϕ : G ≃* G), H ≤ Subgroup.map ϕ.toMonoidHom H
-- Mathlib.FieldTheory.Galois.Infinite
/-- For a subgroup `H` of `Gal(K/k)`, the fixed field of the image of `H` under the restriction to
a normal intermediate field `E` is equal to the fixed field of `H` in `K` intersecting with `E`.  -/
InfiniteGalois.restrict_fixedField : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] (H : Subgroup Gal(K/k))
  (L : IntermediateField k K) [inst_3 : Normal k ↥L],
  IntermediateField.fixedField H ⊓ L =
    IntermediateField.lift (IntermediateField.fixedField (Subgroup.map (AlgEquiv.restrictNormalHom ↥L) H))
-- Mathlib.Algebra.Group.Subgroup.Finite
AddSubgroup.instFiniteSubtypeMem : ∀ {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G) [Finite G], Finite ↥K
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.adjoin_le_centralizer_centralizer : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] (s : Set A),
  NonUnitalStarAlgebra.adjoin R s ≤ NonUnitalStarSubalgebra.centralizer R ↑(NonUnitalStarSubalgebra.centralizer R s)
-- Lean.CoreM
Lean.Core.instInhabitedCache.default : Lean.Core.Cache