mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
CategoryTheory.Functor.ReflectsFiniteEffectiveEpiFamilies.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D},
  (∀ {α : Type} [Finite α] {B : C} (X : α → C) (π : (a : α) → X a ⟶ B),
      (CategoryTheory.EffectiveEpiFamily (fun a => F.obj (X a)) fun a => F.map (π a)) →
        CategoryTheory.EffectiveEpiFamily X π) →
    F.ReflectsFiniteEffectiveEpiFamilies
-- Mathlib.Algebra.LinearRecurrence
/-- **Alias** of `LinearRecurrence.eq_iff_eqOn_range_order`.

---

Two solutions are equal iff their initial conditions are equal.  -/
LinearRecurrence.sol_eq_of_eq_init : ∀ {R : Type u_1} [inst : CommSemiring R] (E : LinearRecurrence R) (u v : ℕ → R),
  E.IsSolution u → E.IsSolution v → (u = v ↔ Set.EqOn u v ↑(Finset.range E.order))
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.ofHom_comp : ∀ {M N P : Type u} [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : Monoid P] (f : M →* N) (g : N →* P),
  MonCat.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (MonCat.ofHom f) (MonCat.ofHom g)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RciSliceData.range : {α : Type u} → {β : Type v} → [inst : Ord α] → Std.DTreeMap.Internal.Const.RciSliceData α β → Std.Rci α
-- Mathlib.Control.Traversable.Lemmas
Traversable.map_traverse' : ∀ {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] {G : Type u → Type u} [inst_2 : Applicative G]
  [LawfulApplicative G] {α β γ : Type u} (g : α → G β) (h : β → γ),
  traverse (Functor.map h ∘ g) = Functor.map (Functor.map h) ∘ traverse g
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiable.add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {f g : M → E'}, MDiff f → MDiff g → MDiff (f + g)
-- Mathlib.Algebra.Order.Hom.Basic
MulRingNormClass.toAddGroupNormClass : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} [inst : NonAssocRing α] [inst_1 : Semiring β]
  [inst_2 : PartialOrder β] [inst_3 : FunLike F α β] [self : MulRingNormClass F α β], AddGroupNormClass F α β
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.spanning_iff_eRk_le' : ∀ {α : Type u_1} {M : Matroid α} {X : Set α} [M.RankFinite], M.Spanning X ↔ M.eRank ≤ M.eRk X ∧ X ⊆ M.E
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- **Alias** of `MonoidAlgebra.toRingHom_mapAlgHom`. -/
MonoidAlgebra.toRingHom_mapRangeAlgHom : ∀ {R : Type u_1} {A : Type u_4} {B : Type u_5} (M : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Monoid M] (f : A →ₐ[R] B),
  ↑(MonoidAlgebra.mapAlgHom M f) = MonoidAlgebra.mapRingHom M f.toRingHom
-- Mathlib.Logic.Function.Basic
Function.Injective.piMap : ∀ {ι : Sort u_4} {α : ι → Sort u_5} {β : ι → Sort u_6} {f : (i : ι) → α i → β i},
  (∀ (i : ι), Function.Injective (f i)) → Function.Injective (Pi.map f)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
/-- The proposition that an affine point `(x, y)` on a Weierstrass curve `W` is nonsingular.

In other words, either `W_X(x, y) ≠ 0` or `W_Y(x, y) ≠ 0`.

Note that this definition is only mathematically accurate for fields.  -/
WeierstrassCurve.Affine.Nonsingular : {R : Type r} → [CommRing R] → WeierstrassCurve.Affine R → R → R → Prop
-- Lean.Elab.Do.Basic
Lean.Elab.Do.doElabToSyntax : {α : Type} →
  Lean.MessageData →
    Lean.Elab.Do.DoElabM Lean.Expr →
      (Lean.Term → Lean.Elab.Do.DoElabM α) → optParam Lean.Syntax Lean.Syntax.missing → Lean.Elab.Do.DoElabM α
-- Mathlib.FieldTheory.KrullTopology
krullTopology_discreteTopology_of_finiteDimensional : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [FiniteDimensional K L],
  DiscreteTopology Gal(L/K)
-- Init.Data.Option.Basic
Option.all_none : ∀ {α : Type u_1} {p : α → Bool}, Option.all p none = true
-- Mathlib.Algebra.Order.Hom.Ring
/-- Reinterpret an ordered ring homomorphism as an ordered additive monoid homomorphism.  -/
OrderRingHom.toOrderAddMonoidHom : {α : Type u_2} →
  {β : Type u_3} →
    [inst : NonAssocSemiring α] →
      [inst_1 : Preorder α] → [inst_2 : NonAssocSemiring β] → [inst_3 : Preorder β] → α →+*o β → α →+o β
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.isoMk₃_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 3}
  (app₀ : f.obj' 0 _proof_297✝ ≅ g.obj' 0 _proof_297✝) (app₁ : f.obj' 1 _proof_298✝ ≅ g.obj' 1 _proof_298✝)
  (app₂ : f.obj' 2 _proof_299✝ ≅ g.obj' 2 _proof_299✝) (app₃ : f.obj' 3 _proof_300✝ ≅ g.obj' 3 _proof_300✝)
  (w₀ :
    CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_298✝)
        app₁.hom =
      CategoryTheory.CategoryStruct.comp app₀.hom
        (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_298✝))
  (w₁ :
    CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_299✝) app₂.hom =
      CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 _proof_246✝ _proof_299✝))
  (w₂ :
    CategoryTheory.CategoryStruct.comp (f.map' 2 3 _proof_299✝ _proof_300✝) app₃.hom =
      CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 2 3 _proof_299✝ _proof_300✝)),
  (CategoryTheory.ComposableArrows.isoMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).hom =
    CategoryTheory.ComposableArrows.homMk₃ app₀.hom app₁.hom app₂.hom app₃.hom w₀ w₁ w₂
-- Plausible.Testable
/-- Enable tracing of all attempted values during shrinking.
 -/
Plausible.Configuration.traceShrinkCandidates : Plausible.Configuration → Bool
-- Mathlib.Tactic.Lift
/-- Main function for the `lift` tactic.  -/
Mathlib.Tactic.Lift.main : Lean.TSyntax `term →
  Lean.TSyntax `term →
    Option (Lean.TSyntax `term) →
      Option (Lean.TSyntax `ident) → Option (Lean.TSyntax `ident) → Bool → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
continuousMultilinearCurryRightEquiv_apply' : ∀ {𝕜 : Type u} {n : ℕ} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] [inst_3 : NormedAddCommGroup G'] [inst_4 : NormedSpace 𝕜 G'] (f : G [×n.succ]→L[𝕜] G')
  (v : Fin n → G) (x : G), (((continuousMultilinearCurryRightEquiv' 𝕜 n G G') f) v) x = f (Fin.snoc v x)
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.eq_symm_apply : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} (e : AddConstEquiv G H a b) {a_1 : H}
  {b_1 : G}, b_1 = e.symm a_1 ↔ e b_1 = a_1
-- Mathlib.Algebra.Free
FreeMagma.lift.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Mul β],
  FreeMagma.lift =
    { toFun := fun f => { toFun := FreeMagma.liftAux f, map_mul' := ⋯ }, invFun := fun F => ⇑F ∘ FreeMagma.of,
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Topology.Hom.Open
/-- Composition of `ContinuousOpenMap`s as a `ContinuousOpenMap`.  -/
ContinuousOpenMap.comp : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : TopologicalSpace α] →
        [inst_1 : TopologicalSpace β] → [inst_2 : TopologicalSpace γ] → (β →CO γ) → (α →CO β) → α →CO γ
-- Mathlib.Data.Nat.Fib.Zeckendorf
_private.Mathlib.Data.Nat.Fib.Zeckendorf.0.Nat.zeckendorf.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.Finite.loopyOn_finite : ∀ {α : Type u_1} {E : Set α}, E.Finite → (Matroid.loopyOn E).Finite
-- Init.Data.Array.Lemmas
Array.anyM.loop.congr_simp : ∀ {α : Type u} {m : Type → Type w} [inst : Monad m] (p p_1 : α → m Bool),
  p = p_1 →
    ∀ (as as_1 : Array α) (e_as : as = as_1) (stop stop_1 : ℕ) (e_stop : stop = stop_1) (h : stop ≤ as.size)
      (j j_1 : ℕ), j = j_1 → Array.anyM.loop p as stop h j = Array.anyM.loop p_1 as_1 stop_1 ⋯ j_1
-- Mathlib.NumberTheory.Real.GoldenRatio
Real.one_sub_goldenConj : 1 - Real.goldenRatio = Real.goldenConj
-- Lean.Parser.Extension
/-- Number of syntax nodes produced by this parser. `none` means "sum of input sizes".  -/
Lean.Parser.ParserAliasInfo.stackSz? : Lean.Parser.ParserAliasInfo → Option ℕ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_eq_some_get : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {a : α}
  (h : a ∈ t), Std.DTreeMap.Const.get? t a = some (Std.DTreeMap.Const.get t a h)
-- Mathlib.Topology.ContinuousMap.Lattice
ContinuousMap.mabs_apply : ∀ {α : Type u_1} [inst : TopologicalSpace α] {β : Type u_2} [inst_1 : TopologicalSpace β] [inst_2 : Group β]
  [inst_3 : IsTopologicalGroup β] [inst_4 : Lattice β] [inst_5 : TopologicalLattice β] (f : C(α, β)) (x : α),
  |f|ₘ x = |f x|ₘ
-- Mathlib.Topology.Semicontinuity.Defs
UpperHemicontinuous.upperHemicontinuousOn : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β},
  UpperHemicontinuous f → ∀ (s : Set α), UpperHemicontinuousOn f s
-- Mathlib.Tactic.FunProp.Theorems
/-- Identity theorem e.g. `Continuous fun x ↦ x`  -/
Mathlib.Meta.FunProp.LambdaTheoremType.id : Mathlib.Meta.FunProp.LambdaTheoremType
-- Mathlib.CategoryTheory.PathCategory.MorphismProperty
/-- A reformulation of `CategoryTheory.Paths.induction'` in terms of `MorphismProperty`.  -/
CategoryTheory.Paths.morphismProperty_eq_top' : ∀ (V : Type u₁) [inst : Quiver V] (P : CategoryTheory.MorphismProperty (CategoryTheory.Paths V)),
  (∀ {v : V}, P (CategoryTheory.CategoryStruct.id ((CategoryTheory.Paths.of V).obj v))) →
    (∀ {u v w : V} (p : u ⟶ v) (q : (CategoryTheory.Paths.of V).obj v ⟶ (CategoryTheory.Paths.of V).obj w),
        P q → P (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Paths.of V).map p) q)) →
      P = ⊤
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- When `S₁.f`, `S₁.g`, `S₂.f` and `S₂.g` are all zero, the action on left homology of a
morphism `φ : S₁ ⟶ S₂` is given by the action `φ.τ₂` on the middle objects.  -/
CategoryTheory.ShortComplex.LeftHomologyMapData.ofZeros : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (φ : S₁ ⟶ S₂) →
          (hf₁ : S₁.f = 0) →
            (hg₁ : S₁.g = 0) →
              (hf₂ : S₂.f = 0) →
                (hg₂ : S₂.g = 0) →
                  CategoryTheory.ShortComplex.LeftHomologyMapData φ
                    (CategoryTheory.ShortComplex.LeftHomologyData.ofZeros S₁ hf₁ hg₁)
                    (CategoryTheory.ShortComplex.LeftHomologyData.ofZeros S₂ hf₂ hg₂)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SolverExtensionState : Type
-- Mathlib.Analysis.Calculus.Deriv.Slope
/-- **Alias** of the forward direction of `hasDerivAt_iff_tendsto_slope_zero`. -/
HasDerivAt.tendsto_slope_zero : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜},
  HasDerivAt f f' x → Filter.Tendsto (fun t => t⁻¹ • (f (x + t) - f x)) (nhdsWithin 0 {0}ᶜ) (nhds f')
-- Mathlib.Data.Finset.Functor
Finset.bind_def : ∀ [inst : (P : Prop) → Decidable P] {α β : Type u_1}, (fun x1 x2 => x1 >>= x2) = Finset.sup
-- Init.Grind.Ring.CommSemiringAdapter
_private.Init.Grind.Ring.CommSemiringAdapter.0.Lean.Grind.CommRing.Expr.denoteS.match_1.eq_7 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (a b : Lean.Grind.CommRing.Expr)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_3 : (v : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var v))
  (h_4 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b))
  (h_6 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k))
  (h_7 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b)) (h_8 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_9 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k)),
  (match a.sub b with
    | Lean.Grind.CommRing.Expr.num k => h_1 k
    | Lean.Grind.CommRing.Expr.natCast k => h_2 k
    | Lean.Grind.CommRing.Expr.var v => h_3 v
    | a.add b => h_4 a b
    | a.mul b => h_5 a b
    | a.pow k => h_6 a k
    | a.sub b => h_7 a b
    | a.neg => h_8 a
    | Lean.Grind.CommRing.Expr.intCast k => h_9 k) =
    h_7 a b
-- Batteries.Recycling.MonadSatisfying.Array
_private.Batteries.Recycling.MonadSatisfying.Array.0.Array.foldlM.loop.match_1.splitter : (motive : ℕ → Sort u_1) → (i : ℕ) → (Unit → motive 0) → ((i' : ℕ) → motive i'.succ) → motive i
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instCommRingOfMulOpposite.eq_1 : ∀ {M : Type u_1} [inst : CommRing Mᵐᵒᵖ], DomMulAct.instCommRingOfMulOpposite = inst
-- Mathlib.Order.WellFoundedSet
Set.Finite.isPWO : ∀ {α : Type u_2} [inst : Preorder α] {s : Set α}, s.Finite → s.IsPWO
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
/-- The point `faceOppositeCentroid` of an n-simplex can be obtained from
the centroid by adding `n⁻¹` times the vector from the vertex to the centroid.  -/
Affine.Simplex.faceOppositeCentroid_eq_smul_vsub_vadd_point : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : NeZero n] [CharZero k] (s : Affine.Simplex k P n) (i : Fin (n + 1)),
  s.faceOppositeCentroid i = (↑n)⁻¹ • (s.centroid -ᵥ s.points i) +ᵥ s.centroid
-- Mathlib.Data.Quot
Quotient.mk''_eq_mk : ∀ {α : Sort u_1} {s : Setoid α}, Quotient.mk'' = Quotient.mk s
-- Mathlib.Computability.Partrec
Nat.Partrec.below.right : ∀ {motive : (a : ℕ →. ℕ) → Nat.Partrec a → Prop}, Nat.Partrec.below Nat.Partrec.right
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.HasLeftHomology.hasCokernel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [S.HasLeftHomology] [inst_3 : CategoryTheory.Limits.HasKernel S.g],
  CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.lift S.g S.f ⋯)
-- Mathlib.Analysis.Meromorphic.Order
/-- Variant of `MeromorphicOn.exists_meromorphicOrderAt_ne_top_iff_forall`, with membership in lieu of
subtypes.
 -/
MeromorphicOn.exists_meromorphicOrderAt_ne_top_iff_forall_mem : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜},
  MeromorphicOn f U → IsConnected U → ((∃ u ∈ U, meromorphicOrderAt f u ≠ ⊤) ↔ ∀ u ∈ U, meromorphicOrderAt f u ≠ ⊤)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.exsphere_univ : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n),
  s.exsphere Finset.univ = s.insphere
-- Mathlib.Data.Nat.Sqrt
Nat.exists_mul_self : ∀ (x : ℕ), (∃ n, n * n = x) ↔ x.sqrt * x.sqrt = x
-- Lean.Elab.Tactic.Try
/-- `evalSuggest` for a sequence of tactics.  -/
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.evalSuggestSeq : Array (Lean.TSyntax `tactic) → Lean.Elab.Tactic.Try.TryTacticM (Lean.TSyntax `tactic)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.coeff_mul_left : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : Group G] [inst_2 : MulSemiringAction G k]
  (f g : SkewMonoidAlgebra k G) (x : G), (f * g).coeff x = f.sum fun a b => b * a • g.coeff (a⁻¹ * x)
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.derivative_expand : ∀ {R : Type u} [inst : CommSemiring R] (p : ℕ) (f : Polynomial R),
  Polynomial.derivative ((Polynomial.expand R p) f) =
    (Polynomial.expand R p) (Polynomial.derivative f) * (↑p * Polynomial.X ^ (p - 1))
-- Mathlib.Order.SupIndep
iSupIndep_comp_coe_iff_supIndep : ∀ {α : Type u_1} {ι : Type u_3} [inst : CompleteLattice α] {s : Finset ι} {f : ι → α},
  iSupIndep (f ∘ Subtype.val) ↔ s.SupIndep f
-- Mathlib.Order.CountableSupClosed
countableSupClosure_min : ∀ {α : Type u_2} {s t : Set α} [inst : Preorder α], s ⊆ t → CountableSupClosed t → countableSupClosure s ⊆ t
-- Mathlib.Order.Antisymmetrization
AntisymmRel.symmGen_congr_left : ∀ {α : Type u_1} {a b c : α} [inst : Preorder α],
  AntisymmRel (fun x1 x2 => x1 ≤ x2) a b →
    (Relation.SymmGen (fun x1 x2 => x1 ≤ x2) a c ↔ Relation.SymmGen (fun x1 x2 => x1 ≤ x2) b c)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get!_eq_default_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {a : α} [inst_2 : Inhabited (β a)], t.contains a = false → t.get! a = default
-- Mathlib.Order.DirectedInverseSystem
/-- Splitting off the `X i` factor from the Pi type over `{j | j ≤ i}`.  -/
InverseSystem.piSplitLE : {ι : Type u_6} →
  {X : ι → Type u_8} →
    {i : ι} → [inst : PartialOrder ι] → [DecidableEq ι] → InverseSystem.piLT X i × X i ≃ ((j : ↑(Set.Iic i)) → X ↑j)
-- Mathlib.Topology.Instances.Rat
Int.isClosedEmbedding_coe_rat : Topology.IsClosedEmbedding Int.cast
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_of_contains_insertMany_list : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List ((a : α) × β a)} {k : α},
      (↑(m.insertMany l)).contains k = true → (List.map Sigma.fst l).contains k = false → m.contains k = true
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rxc.Iterator.Monadic.step.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α] (it : Std.IterM Id α),
  Std.Rxc.Iterator.Monadic.step it =
    match it.internalState.next with
    | none => Std.IterStep.done
    | some next =>
      if next ≤ it.internalState.upperBound then
        Std.IterStep.yield
          { internalState := { next := Std.PRange.succ? next, upperBound := it.internalState.upperBound } } next
      else Std.IterStep.done
-- Mathlib.Data.Int.Init
Int.div_le_div_iff_of_dvd_of_neg_of_pos : ∀ {a b c d : ℤ}, b < 0 → 0 < d → b ∣ a → d ∣ c → (a / b ≤ c / d ↔ c * b ≤ d * a)
-- Mathlib.Data.Complex.Basic
Complex.div_re : ∀ (z w : ℂ), (z / w).re = z.re * w.re / Complex.normSq w + z.im * w.im / Complex.normSq w
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.isSymmetric_iff_isSelfAdjoint : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] (A : E →ₗ[𝕜] E), A.IsSymmetric ↔ IsSelfAdjoint A
-- Mathlib.Algebra.Group.Action.End
MulDistribMulAction.toMulEquiv_symm_apply : ∀ {G : Type u_1} (M : Type u_2) [inst : Group G] [inst_1 : Monoid M] [inst_2 : MulDistribMulAction G M] (x : G) (a : M),
  (MulDistribMulAction.toMulEquiv M x).symm a = x⁻¹ • a
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_eq_getD_default : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited β] {a : α}, m[a]! = m.getD a default
-- Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
AddMonoidAlgebra.instIsDomainOfIsCancelAddOfUniqueSums : ∀ {R : Type u_1} {A : Type u_2} [inst : Semiring R] [IsCancelAdd R] [IsDomain R] [inst_3 : AddMonoid A] [UniqueSums A],
  IsDomain (AddMonoidAlgebra R A)
-- Mathlib.LinearAlgebra.Trace
LinearMap.trace_conj' : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : M →ₗ[R] M) (e : M ≃ₗ[R] N),
  (LinearMap.trace R N) (e.conj f) = (LinearMap.trace R M) f
-- Aesop.Tree.Data
Aesop.Goal.unsafeRulesSelected : Aesop.Goal → Bool
-- Mathlib.Algebra.Module.Defs
Module.mk : {R : Type u} →
  {M : Type v} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [toDistribMulAction : DistribMulAction R M] →
          (∀ (r s : R) (x : M), (r + s) • x = r • x + s • x) → (∀ (x : M), 0 • x = 0) → Module R M
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Hom.toFun_eq_coe : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] {f : L.Hom M N},
  f.toFun = ⇑f
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
/-- **Integration by parts** (vector-valued).
Special case of `integral_smul_deriv_eq_deriv_smul_of_hasDeriv_right`
where the functions have a two-sided derivative in the interior of the interval.  -/
intervalIntegral.integral_smul_deriv_eq_deriv_smul_of_hasDerivAt : ∀ {a b : ℝ} {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra ℝ 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace ℝ E] [CompleteSpace E]
  [IsScalarTower ℝ 𝕜 E] {u u' : ℝ → 𝕜} {v v' : ℝ → E},
  ContinuousOn u (Set.uIcc a b) →
    ContinuousOn v (Set.uIcc a b) →
      (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt u (u' x) x) →
        (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt v (v' x) x) →
          IntervalIntegrable u' MeasureTheory.volume a b →
            IntervalIntegrable v' MeasureTheory.volume a b →
              ∫ (x : ℝ) in a..b, u x • v' x = u b • v b - u a • v a - ∫ (x : ℝ) in a..b, u' x • v x
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {a fallback : α} {c : ℕ},
  (Std.DHashMap.Internal.Raw₀.emptyWithCapacity c).getKeyD a fallback = fallback
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
/-- Lifts along `universalFactorizationMap` corresponds to factorization of `p` into
monic polynomials with fixed degrees.  -/
MvPolynomial.universalFactorizationMapLiftEquiv : (R : Type u_1) →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (n m k : ℕ) →
            (hn : n = m + k) →
              (p : Polynomial.MonicDegreeEq S n) →
                { f //
                    f.comp (MvPolynomial.universalFactorizationMap R n m k hn) =
                      (MvPolynomial.mapEquivMonic R S n).symm p } ≃
                  { q // ↑q.1 * ↑q.2 = ↑p }
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycleOn.apply_mem_iff : ∀ {α : Type u_2} {f : Equiv.Perm α} {s : Set α} {x : α}, f.IsCycleOn s → (f x ∈ s ↔ x ∈ s)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.not_isReal_iff_isComplex : ∀ {K : Type u_1} [inst : Field K] {w : NumberField.InfinitePlace K}, ¬w.IsReal ↔ w.IsComplex
-- Init.Data.Option.Lemmas
Option.bind_join : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {o : Option (Option α)}, o.join.bind f = o.bind fun x => x.bind f
-- Mathlib.Analysis.Complex.Trigonometric
Real.cos_le_one : ∀ (x : ℝ), Real.cos x ≤ 1
-- Mathlib.ModelTheory.Encoding
/-- Decodes a list of variables and function symbols as a list of terms.  -/
FirstOrder.Language.Term.listDecode : {L : FirstOrder.Language} → {α : Type u'} → List (α ⊕ (i : ℕ) × L.Functions i) → List (L.Term α)
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.derivFamily_fp : ∀ {ι : Type u_1} {f : ι → Ordinal.{u} → Ordinal.{u}} [Small.{u, u_1} ι] {i : ι},
  Order.IsNormal (f i) → ∀ (o : Ordinal.{u}), f i (Ordinal.derivFamily f o) = Ordinal.derivFamily f o
-- Mathlib.Algebra.Order.AddGroupWithTop
WithTop.linearOrderedAddCommMonoidWithTop : {α : Type u_2} →
  [inst : AddCancelCommMonoid α] →
    [inst_1 : LinearOrder α] → [IsOrderedAddMonoid α] → LinearOrderedAddCommMonoidWithTop (WithTop α)