mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.BoxIntegral.Partition.Measure
BoxIntegral.Prepartition.measure_iUnion_toReal : ∀ {ι : Type u_1} [Finite ι] {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (μ : MeasureTheory.Measure (ι → ℝ))
  [MeasureTheory.IsLocallyFiniteMeasure μ], μ.real π.iUnion = ∑ J ∈ π.boxes, μ.real ↑J
-- Mathlib.Topology.Compactification.OnePoint.Basic
/-- Extend a homeomorphism of topological spaces
to the homeomorphism of their one point compactifications.  -/
Homeomorph.onePointCongr : {X : Type u_1} →
  {Y : Type u_2} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → X ≃ₜ Y → OnePoint X ≃ₜ OnePoint Y
-- Init.Data.List.Basic
List.isPrefixOf.eq_def : ∀ {α : Type u} [inst : BEq α] (x x_1 : List α),
  x.isPrefixOf x_1 =
    match x, x_1 with
    | [], x => true
    | x, [] => false
    | a :: as, b :: bs => a == b && as.isPrefixOf bs
-- Mathlib.MeasureTheory.Function.UnifTight
/-- Bulk of the proof under strengthened hypotheses. Invoked from `tendsto_Lp_of_tendsto_ae`.  -/
_private.Mathlib.MeasureTheory.Function.UnifTight.0.MeasureTheory.tendsto_Lp_of_tendsto_ae_of_meas : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : NormedAddCommGroup β] {μ : MeasureTheory.Measure α}
  {p : ENNReal},
  1 ≤ p →
    p ≠ ⊤ →
      ∀ {f : ℕ → α → β} {g : α → β},
        (∀ (n : ℕ), MeasureTheory.StronglyMeasurable (f n)) →
          MeasureTheory.StronglyMeasurable g →
            MeasureTheory.MemLp g p μ →
              MeasureTheory.UnifIntegrable f p μ →
                MeasureTheory.UnifTight f p μ →
                  (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) →
                    Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - g) p μ) Filter.atTop (nhds 0)
-- Lean.Parser.Basic
Lean.Parser.sepBy1Info : Lean.Parser.ParserInfo → Lean.Parser.ParserInfo → Lean.Parser.ParserInfo
-- Mathlib.MeasureTheory.Measure.Haar.Unique
MeasureTheory.Measure.haarScalarFactor_eq_integral_div : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (μ' μ : MeasureTheory.Measure G) [inst_5 : μ.IsHaarMeasure]
  [inst_6 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_7 : μ'.IsMulLeftInvariant] {f : G → ℝ},
  Continuous f →
    HasCompactSupport f → ∫ (x : G), f x ∂μ ≠ 0 → ↑(μ'.haarScalarFactor μ) = (∫ (x : G), f x ∂μ') / ∫ (x : G), f x ∂μ
-- Mathlib.RingTheory.Perfection
PreTilt.coeff_frobenius : ∀ {O : Type u₂} [inst : CommRing O] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] [inst_2 : Fact ¬IsUnit ↑p] (n : ℕ)
  (x : PreTilt O p), (PreTilt.coeff (n + 1)) ((frobenius (PreTilt O p) p) x) = (PreTilt.coeff n) x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_insertMany_empty_list_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} [Std.TransOrd α] [inst : BEq α] [Std.LawfulBEqOrd α] {l : List (α × β)}
  {k : α} {fallback : β},
  (List.map Prod.fst l).contains k = false →
    Std.DTreeMap.Internal.Impl.Const.getD
        (↑(Std.DTreeMap.Internal.Impl.Const.insertMany Std.DTreeMap.Internal.Impl.empty l ⋯)) k fallback =
      fallback
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.closure_singleton_zero : ∀ {G : Type u_1} [inst : AddGroup G], AddSubgroup.closure {0} = ⊥
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- The inner product between a multiple of a vector and a `π / 2` rotation of that vector is
zero.  -/
Orientation.inner_rotation_pi_div_two_right_smul : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x : V) (r : ℝ), inner ℝ (r • x) ((o.rotation ↑(Real.pi / 2)) x) = 0
-- Lean.Parser.Basic
Lean.Parser.RecoveryContext.mk.injEq : ∀ (initialPos : String.Pos.Raw) (initialSize : ℕ) (initialPos_1 : String.Pos.Raw) (initialSize_1 : ℕ),
  ({ initialPos := initialPos, initialSize := initialSize } =
      { initialPos := initialPos_1, initialSize := initialSize_1 }) =
    (initialPos = initialPos_1 ∧ initialSize = initialSize_1)
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom.comp.injEq : ∀ {B : Type u} [inst : Quiver B] {a b c : B} (f : CategoryTheory.FreeBicategory.Hom a b)
  (g : CategoryTheory.FreeBicategory.Hom b c) (b_1 : B) (f_1 : CategoryTheory.FreeBicategory.Hom a b_1)
  (g_1 : CategoryTheory.FreeBicategory.Hom b_1 c), (f.comp g = f_1.comp g_1) = (b = b_1 ∧ f ≍ f_1 ∧ g ≍ g_1)
-- Init.System.IO
/-- Fully remove given directory by deleting all contained files and directories in an unspecified order.
Symlinks are deleted but not followed. Fails if any contained entry cannot be deleted or was newly
created during execution.
 -/
IO.FS.removeDirAll : System.FilePath → IO Unit
-- Mathlib.Order.Max
IsMax.eq_1 : ∀ {α : Type u_1} [inst : LE α] (a : α), IsMax a = ∀ ⦃b : α⦄, a ≤ b → b ≤ a
-- Aesop.Forward.State
Aesop.instInhabitedPatSubstSource.default : Aesop.PatSubstSource
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.map_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (x : CategoryTheory.Subobject X),
  (CategoryTheory.Subobject.map (CategoryTheory.CategoryStruct.id X)).obj x = x
-- Mathlib.Lean.Meta
/-- Copy of `Lean.Elab.Tactic.run` that can return a value.  -/
Lean.Elab.Tactic.run_for : {α : Type} → Lean.MVarId → Lean.Elab.Tactic.TacticM α → Lean.Elab.TermElabM (Option α × List Lean.MVarId)
-- Init.Data.List.Perm
List.perm_insert_swap : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] (x y : α) (l : List α),
  (List.insert x (List.insert y l)).Perm (List.insert y (List.insert x l))
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.map_neg : ∀ {𝕜 : 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} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Monoid G] [inst_7 : ContMDiffMul I (↑⊤) G]
  (X : LeftInvariantDerivation I G) (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤), X (-f) = -X f
-- Mathlib.Data.Set.Insert
Set.mem_insert_iff : ∀ {α : Type u_1} {x a : α} {s : Set α}, x ∈ insert a s ↔ x = a ∨ x ∈ s
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.T.induct : ∀ (motive : ℤ → Prop),
  motive 0 →
    motive 1 →
      (∀ (n : ℕ), motive (↑n + 1) → motive ↑n → motive (Int.ofNat n.succ.succ)) →
        (∀ (n : ℕ), motive (-↑n) → motive (-↑n + 1) → motive (Int.negSucc n)) → ∀ (a : ℤ), motive a
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getEntryLE : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      [Std.TransOrd α] →
        (k : α) →
          (t : Std.DTreeMap.Internal.Impl α β) → t.Ordered → (∃ a ∈ t, (compare a k).isLE = true) → (a : α) × β a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.insertManyIfNew_list_equiv_foldl : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ : Std.DTreeMap α β cmp} {l : List ((a : α) × β a)},
  (t₁.insertManyIfNew l).Equiv (List.foldl (fun acc p => acc.insertIfNew p.fst p.snd) t₁ l)
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.getTheoremsForFunction : Lean.Name → Lean.Name → Lean.CoreM (Array Mathlib.Meta.FunProp.FunctionTheorem)
-- Mathlib.Data.Fin.Tuple.Basic
/-- Appending a one-tuple to the right is the same as `Fin.snoc`.  -/
Fin.append_right_eq_snoc : ∀ {α : Sort u_2} {n : ℕ} (x : Fin n → α) (x₀ : Fin 1 → α), Fin.append x x₀ = Fin.snoc x (x₀ 0)
-- Mathlib.Order.OmegaCompletePartialOrder
/-- The supremum of iterating a function on x arbitrary often is smaller than any fixed point.  -/
OmegaCompletePartialOrder.fixedPoints.ωSup_iterate_le_fixedPoint : ∀ {α : Type u_2} [inst : OmegaCompletePartialOrder α] (f : α →𝒄 α) (x : α) (h : x ≤ f x) {a : α},
  a ∈ Function.fixedPoints ⇑f →
    x ≤ a → OmegaCompletePartialOrder.ωSup (OmegaCompletePartialOrder.fixedPoints.iterateChain (↑f) x h) ≤ a
-- Mathlib.Analysis.Normed.Ring.Units
Units.val_add : ∀ {R : Type u_1} [inst : NormedRing R] [inst_1 : HasSummableGeomSeries R] (x : Rˣ) (t : R) (h : ‖t‖ < ‖↑x⁻¹‖⁻¹),
  ↑(x.add t h) = ↑x + t
-- Mathlib.Analysis.Real.OfDigits
Real.ofDigits_le_one : ∀ {b : ℕ} (digits : ℕ → Fin b), Real.ofDigits digits ≤ 1
-- Mathlib.Data.Sign.Defs
SignType.cast.eq_2 : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : Neg α], ↑SignType.pos = 1
-- Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
SimplexCategory.toMk₁_of_castSucc_lt : ∀ {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)),
  j.castSucc < i → (CategoryTheory.ConcreteCategory.hom (SimplexCategory.toMk₁ i)) j = 0
-- Mathlib.Order.Partition.Finpartition
Finpartition.part_eq_iff_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} (P : Finpartition s) {a : α},
  t ∈ P.parts → (P.part a = t ↔ a ∈ t)
-- Mathlib.RingTheory.Perfection
/-- A ring homomorphism `R →+* S` induces `P →+* Q`, a map of the respective perfections.  -/
PerfectionMap.map : (p : ℕ) →
  [inst : Fact (Nat.Prime p)] →
    {R : Type u₁} →
      [inst_1 : CommSemiring R] →
        [inst_2 : CharP R p] →
          {P : Type u₃} →
            [inst_3 : CommSemiring P] →
              [inst_4 : CharP P p] →
                [inst_5 : PerfectRing P p] →
                  {S : Type u₂} →
                    [inst_6 : CommSemiring S] →
                      [inst_7 : CharP S p] →
                        {Q : Type u₄} →
                          [inst_8 : CommSemiring Q] →
                            [inst_9 : CharP Q p] →
                              [inst_10 : PerfectRing Q p] →
                                {π : P →+* R} →
                                  PerfectionMap p π → {σ : Q →+* S} → PerfectionMap p σ → (R →+* S) → P →+* Q
-- Mathlib.Algebra.Group.Conj
/-- Given a conjugacy class `a`, `carrier a` is the set it represents.  -/
ConjClasses.carrier : {α : Type u} → [inst : Monoid α] → ConjClasses α → Set α
-- Mathlib.Topology.Defs.Basic
WithTopology.toTopology.sizeOf_spec : ∀ {X : Type u_1} (t : TopologicalSpace X) [inst : SizeOf X] (ofTopology : X),
  sizeOf (WithTopology.toTopology t ofTopology) = 1 + sizeOf ofTopology
-- Mathlib.Data.Set.Lattice
Set.sUnion_insert : ∀ {α : Type u_1} (s : Set α) (T : Set (Set α)), ⋃₀ insert s T = s ∪ ⋃₀ T
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.logImportFailure : Lean.Meta.RefinedDiscrTree.ImportFailure✝ → Lean.CoreM Unit
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.uniformity_basis_dist : ∀ {α : Type u} [inst : PseudoMetricSpace α], (uniformity α).HasBasis (fun ε => 0 < ε) fun ε => {p | dist p.1 p.2 < ε}
-- Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
Topology.ContinuousMapGeneratedBy.ext_iff : ∀ {ι : Type t} {X : ι → Type u} {inst : (i : ι) → TopologicalSpace (X i)} {Y : Type v} {inst_1 : TopologicalSpace Y}
  {Z : Type v'} {inst_2 : TopologicalSpace Z} {x y : Topology.ContinuousMapGeneratedBy X Y Z}, x = y ↔ x.toFun = y.toFun
-- Lean.Compiler.IR.Basic
Lean.IR.JoinPointId.mk.injEq : ∀ (idx idx_1 : Lean.IR.Index), ({ idx := idx } = { idx := idx_1 }) = (idx = idx_1)
-- Mathlib.Analysis.Real.OfDigits
_private.Mathlib.Analysis.Real.OfDigits.0.Real.b_pos : ∀ {b : ℕ} (digits : ℕ → Fin b), 0 < b
-- Mathlib.ModelTheory.Types
/-- A complete type `p` is realized in a particular structure when there is some
tuple `v` whose type is `p`.  -/
FirstOrder.Language.Theory.realizedTypes : {L : FirstOrder.Language} →
  (T : L.Theory) →
    (M : Type w') → [inst : L.Structure M] → [Nonempty M] → [M ⊨ T] → (α : Type w) → Set (T.CompleteType α)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_minKey? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {em : (a : α) × β a}, Std.Internal.List.minEntry? l = some em → Std.Internal.List.getEntry? em.fst l = some em
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
/-- The discriminant of a polynomial, defined as the determinant of `f.sylvesterDeriv` modified
by a sign. The sign is chosen so polynomials over `ℝ` with all roots real have non-negative
discriminant.  -/
Polynomial.discr : {R : Type u_1} → [inst : CommRing R] → Polynomial R → R
-- Mathlib.Data.Finsupp.Order
Finsupp.le_iff' : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [CanonicallyOrderedAdd α]
  (f g : ι →₀ α) {s : Finset ι}, f.support ⊆ s → (f ≤ g ↔ ∀ i ∈ s, f i ≤ g i)
-- Init.Data.Range.Polymorphic.Nat
Std.instHasRcoIntersectionNat_7 : Std.Ric.HasRcoIntersection ℕ
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- The definition of the "zero" in the colimit is independent of the chosen object
of `J`. In particular, this lemma allows us to "unfold" the definition of `colimit_zero` at
a custom chosen object `j`.  -/
AddMonCat.FilteredColimits.colimit_zero_eq : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCat)
  [inst_1 : CategoryTheory.IsFiltered J] (j : J), 0 = AddMonCat.FilteredColimits.M.mk F ⟨j, 0⟩
-- Mathlib.CategoryTheory.Limits.ExactFunctor
/-- A right exact functor is in particular a functor.  -/
CategoryTheory.RightExactFunctor.forget : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor (C ⥤ᵣ D) (CategoryTheory.Functor C D)
-- Lean.Meta.Tactic.Grind.Cases
Lean.Meta.Grind.CasesEntry.mk : Lean.Name → Bool → Lean.Meta.Grind.CasesEntry
-- Mathlib.Combinatorics.SimpleGraph.Trails
SimpleGraph.Walk.IsEulerian.mem_edges_iff : ∀ {V : Type u_1} {G : SimpleGraph V} [inst : DecidableEq V] {u v : V} {p : G.Walk u v},
  p.IsEulerian → ∀ {e : Sym2 V}, e ∈ p.edges ↔ e ∈ G.edgeSet
-- Mathlib.Data.DFinsupp.Multiset
Multiset.toDFinsupp_le_toDFinsupp : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, Multiset.toDFinsupp s ≤ Multiset.toDFinsupp t ↔ s ≤ t
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.fromIncl_comp_cofanPtIsoSelf_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) (i : X.I),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl i (CategoryTheory.CategoryStruct.id (X.obj i)))
      X.cofanPtIsoSelf.inv =
    (CategoryTheory.Limits.FormalCoproduct.cofan X.I X.toFun).inj i
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.instFibrationP₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.PathObject A)
  [inst_2 : CategoryTheory.Limits.HasBinaryProduct A A] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_4 : CategoryTheory.Limits.HasTerminal C] [(HomotopicalAlgebra.fibrations C).IsStableUnderComposition]
  [(HomotopicalAlgebra.fibrations C).IsStableUnderBaseChange] [HomotopicalAlgebra.IsFibrant A] [P.IsGood],
  HomotopicalAlgebra.Fibration P.p₀
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey!_le : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {k : α}, (compare t.maxKey! k).isLE = true ↔ ∀ k' ∈ t, (compare k' k).isLE = true
-- Init.Data.Slice.List.Lemmas
List.size_mkSlice_rci : ∀ {α : Type u_1} {xs : List α} {lo : ℕ}, Std.Slice.size (Std.Rci.Sliceable.mkSlice xs lo...*) = xs.length - lo
-- Mathlib.Data.QPF.Univariate.Basic
/-- Define the fixed point as the quotient of trees under the equivalence relation `Wequiv`.  -/
QPF.Wsetoid : {F : Type u → Type v} → [q : QPF F] → Setoid (QPF.P F).W
-- Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
HomotopicalAlgebra.instCofibrationInrOfIsCofibrant : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] (X Y : C)
  [(HomotopicalAlgebra.cofibrations C).IsStableUnderCobaseChange]
  [inst_4 : CategoryTheory.Limits.HasBinaryCoproduct X Y] [hX : HomotopicalAlgebra.IsCofibrant X],
  HomotopicalAlgebra.Cofibration CategoryTheory.Limits.coprod.inr
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.addLECancellable_iff_ne_top : ∀ {α : Type u} [inst : Add α] {x : WithTop α} [Nonempty α] [inst_2 : Preorder α] [AddLeftReflectLE α],
  AddLECancellable x ↔ x ≠ ⊤
-- Mathlib.CategoryTheory.Preadditive.FunctorCategory
CategoryTheory.NatTrans.app_sub : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive D]
  {F G : CategoryTheory.Functor C D} (X : C) (α β : F ⟶ G), (α - β).app X = α.app X - β.app X
-- Mathlib.Algebra.Group.Hom.Defs
/-- If `f` is an additive monoid homomorphism then `f 0 = 0`.  -/
AddMonoidHom.map_zero : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZero M] [inst_1 : AddZero N] (f : M →+ N), f 0 = 0
-- Lean.Parser.Command
/-- Adds names from other namespaces to the current namespace.

The command `export Some.Namespace (name₁ name₂)` makes `name₁` and `name₂`:

- visible in the current namespace without prefix `Some.Namespace`, like `open`, and
- visible from outside the current namespace `N` as `N.name₁` and `N.name₂`.

## Examples

```lean
namespace Morning.Sky
  def star := "venus"
end Morning.Sky

namespace Evening.Sky
  export Morning.Sky (star)
  -- `star` is now in scope
  #check star
end Evening.Sky

-- `star` is visible in `Evening.Sky`
#check Evening.Sky.star
```
 -/
Lean.Parser.Command.export : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- Composition of morphisms in the diagram indexing reflexive (co)equalizers  -/
CategoryTheory.Limits.WalkingReflexivePair.Hom.comp : {X Y Z : CategoryTheory.Limits.WalkingReflexivePair} → X.Hom Y → Y.Hom Z → X.Hom Z
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
le_tsub_iff_right : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α], a ≤ c → (b ≤ c - a ↔ b + a ≤ c)
-- Mathlib.Topology.Connected.Separation
/-- A totally separated space is T2.  -/
TotallySeparatedSpace.t2Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [TotallySeparatedSpace X], T2Space X
-- Mathlib.NumberTheory.MulChar.Basic
/-- A multiplicative character `χ` into an integral domain is quadratic
if and only if `χ^2 = 1`.  -/
MulChar.isQuadratic_iff_sq_eq_one : ∀ {M : Type u_4} {R : Type u_5} [inst : CommMonoid M] [inst_1 : CommRing R] [NoZeroDivisors R] [Nontrivial R]
  {χ : MulChar M R}, χ.IsQuadratic ↔ χ ^ 2 = 1
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.nnnorm_zpow_le : ∀ {S : Type u_1} [inst : SeminormedGroup S] [IsUltrametricDist S] (x : S) (z : ℤ), ‖x ^ z‖₊ ≤ ‖x‖₊
-- Lean.PrettyPrinter.Delaborator.Basic
/-- Runs the delaborator `act` with increased depth.
The depth is used when `pp.deepTerms` is `false` to determine what is a deep term.
See also `Lean.PrettyPrinter.Delaborator.Context.depth`.
 -/
Lean.PrettyPrinter.Delaborator.withIncDepth : {α : Type} → Lean.PrettyPrinter.Delaborator.DelabM α → Lean.PrettyPrinter.Delaborator.DelabM α
-- Mathlib.Order.WithBot
WithTop.forall_lt_coe : ∀ {α : Type u_1} {a : α} [inst : Preorder α] {p : WithTop α → Prop}, (∀ x < ↑a, p x) ↔ ∀ b < a, p ↑b
-- Mathlib.Data.Complex.Basic
Complex.div_ofReal : ∀ (z : ℂ) (x : ℝ), z / ↑x = { re := z.re / x, im := z.im / x }
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Augmented.w_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.SimplicialObject.Augmented C} (f : X ⟶ Y)
  (n : SimplexCategoryᵒᵖ),
  CategoryTheory.CategoryStruct.comp (f.left.app n) (Y.hom.app n) =
    CategoryTheory.CategoryStruct.comp (X.hom.app n) f.right
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The tangent of an angle in a right-angled triangle as a ratio of sides.  -/
EuclideanGeometry.tan_oangle_left_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P},
  EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) → (EuclideanGeometry.oangle p₃ p₁ p₂).tan = dist p₃ p₂ / dist p₁ p₂
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
/-- A finite product of monotone functions is monotone.  -/
Monotone.finsetProd' : ∀ {ι : Type u_1} {N : Type u_5} [inst : CommMonoid N] [inst_1 : Preorder N] {s : Finset ι} [MulLeftMono N]
  {γ : Type u_9} [inst_3 : Preorder γ] {f : ι → γ → N}, (∀ i ∈ s, Monotone (f i)) → Monotone fun x => ∏ i ∈ s, f i x
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.PlacedTile.smul_mk_coe : ∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [inst : Group G] [inst_1 : MulAction G X]
  {ps : DiscreteTiling.Protoset G X ιₚ} (g h : G) (i : ιₚ),
  g • { index := i, groupElts := ↑h } = { index := i, groupElts := ↑(g * h) }
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.B_one : CartanMatrix.B 1 = CartanMatrix.A 1
-- Mathlib.Algebra.Homology.Factorizations.CM5a
/-- A section of `π K L n₁`  -/
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.σ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (K L : CochainComplex C ℤ) →
        [inst_2 : CategoryTheory.EnoughInjectives C] →
          (n₁ : ℤ) → L ⟶ CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.mid✝ K L n₁
-- Mathlib.Data.Multiset.UnionInter
Multiset.union_add_inter : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α), s ∪ t + s ∩ t = s + t
-- Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
ruzsaSzemerediNumberNat_two : ruzsaSzemerediNumberNat 2 = 0
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.entryAtIdx!.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Inhabited ((a : α) × β a)] (x size : ℕ) (k : α) (v : β k)
  (l r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k v l r).entryAtIdx! x =
    match compare x l.size with
    | Ordering.lt => l.entryAtIdx! x
    | Ordering.eq => ⟨k, v⟩
    | Ordering.gt => r.entryAtIdx! (x - l.size - 1)
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.Monic.normalize_eq_self : ∀ {R : Type u} [inst : CommRing R] [inst_1 : NoZeroDivisors R] [inst_2 : NormalizationMonoid R] {p : Polynomial R},
  p.Monic → normalize p = p
-- Init.Data.Option.Lemmas
Option.get!_join : ∀ {α : Type u_1} [inst : Inhabited α] {x : Option (Option α)}, x.join.get! = x.get!.get!
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
AlternatingMap.mkContinuousAlternating_norm_le : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : Fintype ι]
  {ι' : Type u_1} [inst_8 : Fintype ι'] (f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G) {C : ℝ},
  0 ≤ C →
    ∀ (H : ∀ (m₁ : ι → E) (m₂ : ι' → F), ‖(f m₁) m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖),
      ‖f.mkContinuousAlternating C H‖ ≤ C
-- Mathlib.RingTheory.Polynomial.HilbertPoly
Polynomial.natDegree_hilbertPoly_of_ne_zero : ∀ {F : Type u_1} [inst : Field F] [CharZero F] {p : Polynomial F} {d : ℕ},
  p.hilbertPoly d ≠ 0 → (p.hilbertPoly d).natDegree = d - Polynomial.rootMultiplicity 1 p - 1
-- Mathlib.Data.Set.Restrict
Set.restrictPreimage_surjective : ∀ {α : Type u_1} {β : Type u_2} (t : Set β) {f : α → β},
  Function.Surjective f → Function.Surjective (t.restrictPreimage f)
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instAddCommGroup : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : AddCommGroup β] → [IsTopologicalAddGroup β] → AddCommGroup (ZeroAtInftyContinuousMap α β)