mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Util.Export
Lean.Export.instInhabitedAlloc.default : {α : Type u_1} → {inst : BEq α} → {inst_1 : Hashable α} → Lean.Export.Alloc α
-- Mathlib.Data.Finset.Empty
Finset.isEmpty_coe_sort : ∀ {α : Type u_1} {s : Finset α}, IsEmpty ↥s ↔ s = ∅
-- Init.Data.Nat.Lemmas
Nat.pow_right_inj : ∀ {a m n : ℕ}, 1 < a → (a ^ m = a ^ n ↔ m = n)
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.denote'_add : ∀ (ctx : Int.Internal.Linear.Context) (a : ℤ) (x : Int.Internal.Linear.Var) (p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.Poly.denote' ctx (Int.Internal.Linear.Poly.add a x p) =
    a * Int.Internal.Linear.Var.denote ctx x + Int.Internal.Linear.Poly.denote ctx p
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey_unitOfList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a == b) = false) l →
      k ∈ l → ∀ {h : k' ∈ Std.DHashMap.Const.unitOfList l}, (Std.DHashMap.Const.unitOfList l).getKey k' h = k
-- Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
MeasureTheory.MemLp.add : ∀ {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε]
  {p : ENNReal} {μ : MeasureTheory.Measure α} {f g : α → ε} [ContinuousAdd ε],
  MeasureTheory.MemLp f p μ → MeasureTheory.MemLp g p μ → MeasureTheory.MemLp (f + g) p μ
-- Init.Data.UInt.Bitwise
USize.toNat_and : ∀ (a b : USize), (a &&& b).toNat = a.toNat &&& b.toNat
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.sup_eq_add : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (I J : FractionalIdeal S P), I ⊔ J = I + J
-- Mathlib.Order.Filter.Bases.Finite
Filter.FilterBasis.ofSets_sets : ∀ {α : Type u_1} (s : Set (Set α)), (Filter.FilterBasis.ofSets s).sets = Set.sInter '' {t | t.Finite ∧ t ⊆ s}
-- Lean.Elab.Term.TermElabM
_private.Lean.Elab.Term.TermElabM.0.Lean.Elab.Term.elabImplicitLambdaAux : Lean.Syntax → Bool → Lean.Expr → Array Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_one : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R], ⌊1⌋ = 1
-- Batteries.Data.List.Lemmas
List.findIdxs_append : ∀ {α : Type u_1} {xs ys : List α} {p : α → Bool} {s : ℕ},
  List.findIdxs p (xs ++ ys) s = List.findIdxs p xs s ++ List.findIdxs p ys (s + xs.length)
-- Mathlib.RingTheory.Jacobson.Ideal
Ideal.mem_jacobson_bot : ∀ {R : Type u} [inst : CommRing R] {x : R}, x ∈ ⊥.jacobson ↔ ∀ (y : R), IsUnit (x * y + 1)
-- Mathlib.AlgebraicGeometry.Sites.ElladicCohomology
AlgebraicGeometry.Scheme.instAddCommGroupEllAdicCohomology : (X : AlgebraicGeometry.Scheme) →
  (ℓ : ℕ) → [inst : Fact (Nat.Prime ℓ)] → (n : ℕ) → AddCommGroup (X.EllAdicCohomology ℓ n)
-- Mathlib.Topology.TietzeExtension
TietzeExtension.mk : ∀ {Y : Type v} [inst : TopologicalSpace Y],
  (∀ {X : Type u} [inst_1 : TopologicalSpace X] [NormalSpace X] (s : Set X),
      IsClosed s → ∀ (f : C(↑s, Y)), ∃ g, ContinuousMap.restrict s g = f) →
    TietzeExtension Y
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- Each function of a family equicontinuous at `x₀` is continuous at `x₀`.  -/
EquicontinuousAt.continuousAt : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {F : ι → X → α} {x₀ : X},
  EquicontinuousAt F x₀ → ∀ (i : ι), ContinuousAt (F i) x₀
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.isoMk₅_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 5}
  (app₀ : f.obj' 0 _proof_449✝ ≅ g.obj' 0 _proof_449✝) (app₁ : f.obj' 1 _proof_450✝ ≅ g.obj' 1 _proof_450✝)
  (app₂ : f.obj' 2 _proof_451✝ ≅ g.obj' 2 _proof_451✝) (app₃ : f.obj' 3 _proof_452✝ ≅ g.obj' 3 _proof_452✝)
  (app₄ : f.obj' 4 _proof_453✝ ≅ g.obj' 4 _proof_453✝) (app₅ : f.obj' 5 _proof_454✝ ≅ g.obj' 5 _proof_454✝)
  (w₀ :
    CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_450✝)
        app₁.hom =
      CategoryTheory.CategoryStruct.comp app₀.hom
        (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_450✝))
  (w₁ :
    CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_451✝) app₂.hom =
      CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 _proof_246✝ _proof_451✝))
  (w₂ :
    CategoryTheory.CategoryStruct.comp (f.map' 2 3 _proof_299✝ _proof_452✝) app₃.hom =
      CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 2 3 _proof_299✝ _proof_452✝))
  (w₃ :
    CategoryTheory.CategoryStruct.comp (f.map' 3 4 _proof_364✝ _proof_453✝) app₄.hom =
      CategoryTheory.CategoryStruct.comp app₃.hom (g.map' 3 4 _proof_364✝ _proof_453✝))
  (w₄ :
    CategoryTheory.CategoryStruct.comp (f.map' 4 5 _proof_453✝ _proof_454✝) app₅.hom =
      CategoryTheory.CategoryStruct.comp app₄.hom (g.map' 4 5 _proof_453✝ _proof_454✝)),
  (CategoryTheory.ComposableArrows.isoMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).inv =
    CategoryTheory.ComposableArrows.homMk₅ app₀.inv app₁.inv app₂.inv app₃.inv app₄.inv app₅.inv ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.LinearAlgebra.Vandermonde
Matrix.eq_zero_of_forall_index_sum_pow_mul_eq_zero : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} [IsDomain R] {f v : Fin n → R},
  Function.Injective f → (∀ (j : Fin n), ∑ i, f j ^ ↑i * v i = 0) → v = 0
-- Mathlib.Algebra.Algebra.Defs
algebraMap.coe_add : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (a b : R),
  ↑(a + b) = ↑a + ↑b
-- Mathlib.Topology.Category.Sequential
Sequential.instCategory : CategoryTheory.Category.{u, u + 1} Sequential
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.instIsEquivalenceGeneratedByTopCatFromGeneratedByTopCat : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)],
  ContinuousGeneratedByCat.fromGeneratedByTopCat.IsEquivalence
-- Mathlib.RingTheory.PrincipalIdealDomain
Irreducible.coprime_pow_of_not_dvd : ∀ {R : Type u} [inst : CommRing R] [IsBezout R] {p a : R} (m : ℕ), Irreducible p → ¬p ∣ a → IsCoprime a (p ^ m)
-- Mathlib.RingTheory.Invariant.Galois
/-- If the extension `B/Q` over `A/P` is separable, then it is finite dimensional.  -/
Ideal.Quotient.finite_of_isInvariant : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (G : Type u_3)
  [Finite G] [inst_4 : Group G] [inst_5 : MulSemiringAction G B] [Algebra.IsInvariant A B G] (P : Ideal A) (Q : Ideal B)
  [inst_7 : Q.LiesOver P] [P.IsMaximal] [Q.IsMaximal] [SMulCommClass G A B] [Algebra.IsSeparable (A ⧸ P) (B ⧸ Q)],
  Module.Finite (A ⧸ P) (B ⧸ Q)
-- Mathlib.GroupTheory.Perm.Sign
_private.Mathlib.GroupTheory.Perm.Sign.0.Equiv.Perm.signAux2.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Equiv.Perm α → Sort u_2) (x : Equiv.Perm α) (h_1 : (x : Equiv.Perm α) → motive [] x)
  (h_2 : (x : α) → (l : List α) → (f : Equiv.Perm α) → motive (x :: l) f),
  (match [], x with
    | [], x => h_1 x
    | x :: l, f => h_2 x l f) =
    h_1 x
-- Mathlib.Data.Part
Part.add_get_eq : ∀ {α : Type u_1} [inst : Add α] (a b : Part α) (hab : (a + b).Dom), (a + b).get hab = a.get ⋯ + b.get ⋯
-- Mathlib.Topology.Neighborhoods
mem_interior_iff_mem_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s : Set X}, x ∈ interior s ↔ s ∈ nhds x
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctor.comp_mapComp_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {D : Type u₃}
  [inst_2 : CategoryTheory.Bicategory D] (F : CategoryTheory.StrictPseudofunctor B C)
  (G : CategoryTheory.StrictPseudofunctor C D) {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  ((F.comp G).mapComp f g).hom =
    CategoryTheory.CategoryStruct.comp (G.map₂ (F.mapComp f g).hom) (G.mapComp (F.map f) (F.map g)).hom
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast!_insertList_of_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l toInsert : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k k' : α} (k_beq : (k == k') = true) (v : β k) [inst_2 : Inhabited (β k')],
      List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert →
        ⟨k, v⟩ ∈ toInsert → Std.Internal.List.getValueCast! k' (Std.Internal.List.insertList l toInsert) = cast ⋯ v
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Subgraph.Connected.induce_verts : ∀ {V : Type u} {G : SimpleGraph V} {H : G.Subgraph}, H.Connected → (SimpleGraph.induce H.verts G).Connected
-- Mathlib.Algebra.Group.Basic
/-- **Alias** of `multiplicative_of_symm_of_total`. -/
multiplicative_of_symmetric_of_total : ∀ {α : Type u_1} {β : Type u_2} [inst : Monoid β] (p r : α → α → Prop) [Std.Total r] (f : α → α → β) [Std.Symm p],
  (∀ {a b : α}, p a b → f a b * f b a = 1) →
    (∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c) →
      ∀ {a b c : α}, p a b → p b c → p a c → f a c = f a b * f b c
-- Mathlib.CategoryTheory.Abelian.Basic
/-- the cokernel cofork is a a limit  -/
CategoryTheory.Abelian.AbelianStruct.isColimitCokernelCofork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          (self : CategoryTheory.Abelian.AbelianStruct f) → CategoryTheory.Limits.IsColimit self.cokernelCofork
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_sum' : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {s : Finset ι} {X : ι → Ω → ℝ}
  [MeasureTheory.IsFiniteMeasure μ],
  (∀ i ∈ s, MeasureTheory.MemLp (X i) 2 μ) →
    ProbabilityTheory.variance (∑ i ∈ s, X i) μ = ∑ i ∈ s, ∑ j ∈ s, ProbabilityTheory.covariance (X i) (X j) μ
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.size.eq_1 : ∀ {α : Type u} {β : α → Type v} (sz : ℕ) (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner sz k v l r).size = sz
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
/-- If `f` is nonnegative a.e.-everywhere and it is integrable on the unordered interval
`Set.uIoc a b`, then its integral over `a..b` is positive if and only if `a < b` and the
measure of `Function.support f ∩ Set.Ioc a b` is positive.  -/
intervalIntegral.integral_pos_iff_support_of_nonneg_ae : ∀ {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
  0 ≤ᵐ[μ] f →
    IntervalIntegrable f μ a b → (0 < ∫ (x : ℝ) in a..b, f x ∂μ ↔ a < b ∧ 0 < μ (Function.support f ∩ Set.Ioc a b))
-- Mathlib.Algebra.Order.Group.Opposite
MulOpposite.op_le_one : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] {a : α}, MulOpposite.op a ≤ 1 ↔ a ≤ 1
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
SimpleGraph.componentComplMk.congr_simp : ∀ {V : Type u} {K : Set V} (G : SimpleGraph V) {v v_1 : V} (e_v : v = v_1) (vK : v ∉ K),
  G.componentComplMk vK = G.componentComplMk ⋯
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey_insertIfNew_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, t.isEmpty = true → (t.insertIfNew k v).minKey ⋯ = k
-- Mathlib.AlgebraicTopology.Reedy.Basic
HomotopicalAlgebra.ReedyStructure.degHom_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [inst_1 : W₁.IsMultiplicative] [inst_2 : W₂.IsMultiplicative] {α : Type u_2} [inst_3 : LinearOrder α]
  [inst_4 : OrderBot α] [inst_5 : SuccOrder α] [inst_6 : WellFoundedLT α]
  (r : HomotopicalAlgebra.ReedyStructure W₁ W₂ α) {X Y : C} {f : X ⟶ Y} (h : W₁.MapFactorizationData W₂ f),
  r.degHom f = r.deg h.Z
-- Mathlib.Order.Hom.Bounded
BotHom.copy.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Bot α] [inst_1 : Bot β] (f : BotHom α β) (f' : α → β) (h : f' = ⇑f),
  f.copy f' h = { toFun := f', map_bot' := ⋯ }
-- Mathlib.Algebra.GroupWithZero.Indicator
Set.indicator_eq_zero_iff_notMem : ∀ {ι : Type u_1} (M₀ : Type u_4) [inst : MulZeroOneClass M₀] {s : Set ι} {i : ι} [Nontrivial M₀],
  s.indicator 1 i = 0 ↔ i ∉ s
-- Mathlib.Probability.Moments.IntegrableExpMul
/-- If `v` belongs to the interior of the interval `integrableExpSet X μ`,
then `|X| ^ n * exp (v * X)` is integrable for all `n : ℕ`.  -/
ProbabilityTheory.integrable_pow_abs_mul_exp_of_mem_interior_integrableExpSet : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {v : ℝ},
  v ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    ∀ (n : ℕ), MeasureTheory.Integrable (fun ω => |X ω| ^ n * Real.exp (v * X ω)) μ
-- Lean.Meta.AppBuilder
/-- Given `h : a = b`, returns a proof of `a ≍ b`.  -/
Lean.Meta.mkHEqOfEq : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.prodUnique_symm_apply : ∀ (R : Type u_8) (M : Type u_9) (N : Type u_10) [inst : Semiring R] [inst_1 : TopologicalSpace M]
  [inst_2 : AddCommMonoid M] [inst_3 : TopologicalSpace N] [inst_4 : AddCommMonoid N] [inst_5 : Unique N]
  [inst_6 : Module R M] [inst_7 : Module R N] (x : M), (ContinuousLinearEquiv.prodUnique R M N).symm x = (x, default)
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.CommShift.OfComp.iso.congr_simp : ∀ {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]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} {H : CategoryTheory.Functor C E}
  (e e_1 : F.comp G ≅ H),
  e = e_1 →
    ∀ [inst_3 : G.Full] [inst_4 : G.Faithful] {A : Type u_5} [inst_5 : AddMonoid A]
      [inst_6 : CategoryTheory.HasShift C A] [inst_7 : CategoryTheory.HasShift D A]
      [inst_8 : CategoryTheory.HasShift E A] [inst_9 : G.CommShift A] [inst_10 : H.CommShift A] (a : A),
      CategoryTheory.Functor.CommShift.OfComp.iso e a = CategoryTheory.Functor.CommShift.OfComp.iso e_1 a
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.isAcyclic_iff_path_unique : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsAcyclic ↔ ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q
-- Std.Http.Protocol.H1.Writer
Std.Http.Protocol.H1.Writer.State.writingBodyClosingFrame.sizeOf_spec : sizeOf Std.Http.Protocol.H1.Writer.State.writingBodyClosingFrame = 1
-- Init.Data.SInt.Lemmas
Int16.toISize_mod : ∀ (a b : Int16), (a % b).toISize = a.toISize % b.toISize
-- Init.Data.String.TakeDrop
String.Internal.dropRightImpl : String → ℕ → String
-- Mathlib.Analysis.Distribution.TemperateGrowth
Function.Complex.hasTemperateGrowth_ofReal : Function.HasTemperateGrowth Complex.ofReal
-- Mathlib.Algebra.Polynomial.Basic
/-- `coeff p n` (often denoted `p.coeff n`) is the coefficient of `X^n` in `p`.  -/
Polynomial.coeff : {R : Type u} → [inst : Semiring R] → Polynomial R → ℕ → R
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.NatStruct.addFn : Lean.Meta.Grind.Arith.Linear.NatStruct → Lean.Expr
-- Mathlib.Topology.Bases
isTopologicalBasis_subtype : ∀ {α : Type u_1} [inst : TopologicalSpace α] {B : Set (Set α)},
  TopologicalSpace.IsTopologicalBasis B →
    ∀ (p : α → Prop), TopologicalSpace.IsTopologicalBasis (Set.preimage Subtype.val '' B)
-- Mathlib.Algebra.Homology.ShortComplex.Limits
CategoryTheory.ShortComplex.instPreservesFiniteLimitsπ₃ : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{v_2, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasFiniteLimits C], CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.ShortComplex.π₃
-- Std.Time.DateTime
/-- Getter for the `Nanosecond` inside of a `DateTime`
 -/
Std.Time.DateTime.nanosecond : Std.Time.DateTime → Std.Time.Nanosecond.Ordinal
-- Lean.Meta.TransparencyMode
Lean.Meta.TransparencyMode.lt : Lean.Meta.TransparencyMode → Lean.Meta.TransparencyMode → Bool
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.elabCheck : Lean.Elab.Command.CommandElab
-- Mathlib.Data.Nat.Cast.Commute
SemiconjBy.natCast_mul_natCast_mul : ∀ {α : Type u_1} [inst : Semiring α] {a x y : α}, SemiconjBy a x y → ∀ (m n : ℕ), SemiconjBy (↑m * a) (↑n * x) (↑n * y)
-- Std.Net.Addr
Std.Net.IPv6Addr.mk.injEq : ∀ (segments segments_1 : Vector UInt16 8),
  ({ segments := segments } = { segments := segments_1 }) = (segments = segments_1)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α], m₁.WF → m₂.WF → ∀ {k : α} {fallback : β k}, k ∉ m₂ → (m₁ ∩ m₂).getD k fallback = fallback
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `IsAddTorsion.torsionAddEquiv`.

---

A torsion additive monoid is isomorphic to its torsion additive submonoid.  -/
AddMonoid.IsTorsion.torsionAddEquiv : {G : Type u_1} → [inst : AddCommMonoid G] → IsAddTorsion G → ↥(AddCommMonoid.addTorsion G) ≃+ G
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
/-- Evaluation of power series at adequate elements, as a `RingHom`  -/
MvPowerSeries.eval₂Hom : {σ : Type u_1} →
  {R : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : UniformSpace R] →
        {S : Type u_3} →
          [inst_2 : CommRing S] →
            [inst_3 : UniformSpace S] →
              {φ : R →+* S} →
                {a : σ → S} →
                  [IsTopologicalSemiring R] →
                    [IsUniformAddGroup R] →
                      [IsUniformAddGroup S] →
                        [CompleteSpace S] →
                          [T2Space S] →
                            [IsTopologicalRing S] →
                              [IsLinearTopology S S] → Continuous ⇑φ → MvPowerSeries.HasEval a → MvPowerSeries σ R →+* S
-- Init.Data.Nat.Basic
Nat.sub_ne_zero_iff_lt : ∀ {n m : ℕ}, n - m ≠ 0 ↔ m < n
-- Mathlib.Analysis.Normed.Order.Lattice
/-- Let `α` be a normed lattice ordered group. Then the infimum is jointly continuous.
 -/
HasSolidNorm.continuousInf : ∀ {α : Type u_1} [inst : NormedAddCommGroup α] [inst_1 : Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α],
  ContinuousInf α
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
/-- `ιInvApp` is the inverse of `D.ι i` on `U`.  -/
AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_eq_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C)
  [inst_1 : CategoryTheory.Limits.HasLimits C] (i : D.J) (U : TopologicalSpace.Opens ↑↑(D.U i)),
  CategoryTheory.CategoryStruct.comp (D.diagramOverOpenπ U i)
      (CategoryTheory.CategoryStruct.comp (D.ιInvAppπEqMap U) (D.ιInvApp U)) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.limit (D.diagramOverOpen U))
-- Mathlib.Analysis.Analytic.Constructions
/-- Powers of analytic functions (into a normed `𝕜`-algebra) are analytic.  -/
AnalyticOn.pow : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {A : Type u_7} [inst_3 : NormedRing A] [inst_4 : NormedAlgebra 𝕜 A] {f : E → A}
  {s : Set E}, AnalyticOn 𝕜 f s → ∀ (n : ℕ), AnalyticOn 𝕜 (f ^ n) s
-- Lean.Parser.Extra
/-- No-op parser combinator that allows the pretty printer to omit the group and
indent operation in the enclosing category parser.
```
syntax ppAllowUngrouped "by " tacticSeq : term
-- allows a `by` after `:=` without linebreak in between:
theorem foo : True := by
  trivial
```
 -/
Lean.Parser.ppAllowUngrouped : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Abelian.FreydMitchell
CategoryTheory.Abelian.FreydMitchell.instPreservesFiniteColimitsModuleCatEmbeddingRingFunctor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C],
  CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.Abelian.FreydMitchell.functor C)
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.FiniteRangeSetoid.equiv_iff_hasFiniteRange : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : CommRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] [IsNoetherianRing K] {u v : V →ₗ[K] V₂},
  u ≈ v ↔ (u - v).HasFiniteRange
-- Mathlib.AlgebraicTopology.Reedy.Basic
HomotopicalAlgebra.ReedyStructure.lt₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [inst_1 : W₁.IsMultiplicative] [inst_2 : W₂.IsMultiplicative] {α : Type u_2} [inst_3 : LinearOrder α]
  [inst_4 : OrderBot α] [inst_5 : SuccOrder α] [inst_6 : WellFoundedLT α]
  (self : HomotopicalAlgebra.ReedyStructure W₁ W₂ α) {X Y : C} (f : X ⟶ Y),
  W₂ f → ¬CategoryTheory.MorphismProperty.identities C f → self.deg X < self.deg Y
-- Mathlib.NumberTheory.EulerProduct.DirichletLSeries
/-- The Euler product for Dirichlet L-series, valid for `s.re > 1`.
This version is stated in the form of convergence of finite partial products.  -/
DirichletCharacter.LSeries_eulerProduct : ∀ {s : ℂ} {N : ℕ} (χ : DirichletCharacter ℂ N),
  1 < s.re →
    Filter.Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - χ ↑p * ↑p ^ (-s))⁻¹) Filter.atTop
      (nhds (LSeries (fun n => χ ↑n) s))
-- Mathlib.Algebra.Regular.Prod
Prod.isSMulRegular_iff : ∀ {α : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SMul α R] [inst_1 : SMul α S] {r : α} [Nonempty R] [Nonempty S],
  IsSMulRegular (R × S) r ↔ IsSMulRegular R r ∧ IsSMulRegular S r
-- Mathlib.Analysis.Analytic.Order
/-- If an analytic function `f` is not constantly zero on a connected set `U`, then its set of zeros is
codiscrete within `U`.

See `AnalyticOnNhd.preimage_mem_codiscreteWithin` for a more general statement in preimages of
codiscrete sets.
 -/
AnalyticOnNhd.preimage_zero_mem_codiscreteWithin : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {U : Set 𝕜} {f : 𝕜 → E} {x : 𝕜},
  AnalyticOnNhd 𝕜 f U → f x ≠ 0 → x ∈ U → IsConnected U → f ⁻¹' {0}ᶜ ∈ Filter.codiscreteWithin U
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.id_right : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] (f : CategoryTheory.Arrow T),
  CategoryTheory.Arrow.Hom.right (CategoryTheory.CategoryStruct.id f) = CategoryTheory.CategoryStruct.id f.right
-- Init.BinderPredicates
/-- Declare `∀ x ∉ y, ...` as syntax for `∀ x, x ∉ y → ...` and `∃ x ∉ y, ...` as syntax for
`∃ x, x ∉ y ∧ ...`  -/
Lean.«binderPred∉_» : Lean.ParserDescr
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.toList.match_1.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Std.DHashMap.Internal.AssocList α β → Sort u_3)
  (h_1 : Unit → motive Std.DHashMap.Internal.AssocList.nil)
  (h_2 :
    (a : α) →
      (b : β a) → (es : Std.DHashMap.Internal.AssocList α β) → motive (Std.DHashMap.Internal.AssocList.cons a b es)),
  (match Std.DHashMap.Internal.AssocList.nil with
    | Std.DHashMap.Internal.AssocList.nil => h_1 ()
    | Std.DHashMap.Internal.AssocList.cons a b es => h_2 a b es) =
    h_1 ()
-- Mathlib.Data.List.Basic
List.map_reverseAux : ∀ {α : Type u} {β : Type v} (f : α → β) (l₁ l₂ : List α),
  List.map f (l₁.reverseAux l₂) = (List.map f l₁).reverseAux (List.map f l₂)
-- LeanSearchClient.Syntax
LeanSearchClient.SearchServer.searchCommandSuggestions : LeanSearchClient.SearchServer → Lean.Syntax → Lean.TSyntax `str → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- A fan `c` on `f` such that the induced map `c.pt ⟶ ∏ f` is an iso, is a product.  -/
CategoryTheory.Limits.Fan.isLimitOfIsIsoPiLift : {β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f : β → C} →
        [inst_1 : CategoryTheory.Limits.HasProduct f] →
          (c : CategoryTheory.Limits.Fan f) →
            [hc : CategoryTheory.IsIso (CategoryTheory.Limits.Pi.lift c.proj)] → CategoryTheory.Limits.IsLimit c
-- Mathlib.Tactic.CancelDenoms.Core
Mathlib.Tactic.CancelDenoms.inv_subst : ∀ {α : Type u_1} [inst : Field α] {n k e : α}, e ≠ 0 → n * e = k → k * e⁻¹ = n
-- Mathlib.Data.Set.Image
Set.Nontrivial.image_of_injOn : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β}, s.Nontrivial → Set.InjOn f s → (f '' s).Nontrivial
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.End.mul_def : ∀ {M : Type u_2} {X : Type u_4} [inst : SMul M X] {f g : X →ₑ[id] X}, f * g = f.comp g