mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.VectorMeasure.Prod
MeasureTheory.VectorMeasure.variation_prod_le : ∀ {X : Type u_2} {Y : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X}
  {mY : MeasurableSpace Y} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  {μ : MeasureTheory.VectorMeasure X E} {ν : MeasureTheory.VectorMeasure Y F} {B : E →L[ℝ] F →L[ℝ] G} [CompleteSpace G]
  [MeasureTheory.IsFiniteMeasure μ.variation] [MeasureTheory.SFinite ν.variation],
  (μ.prod ν B).variation ≤ ‖B‖ₑ • μ.variation.prod ν.variation
-- Mathlib.Topology.Order.LiminfLimsup
exists_seq_tendsto_liminf : ∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] [FirstCountableTopology α] {f : Filter β} [f.NeBot] {u : β → α} [f.IsCountablyGenerated],
  autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f u) exists_seq_tendsto_liminf._auto_1 →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) exists_seq_tendsto_liminf._auto_3 →
      ∃ x, Filter.Tendsto (u ∘ x) Filter.atTop (nhds (Filter.liminf u f)) ∧ Filter.Tendsto x Filter.atTop f
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.walkingSpanOpEquiv_functor_map : ∀ {X Y : (CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair)ᵒᵖ} (f : X ⟶ Y),
  CategoryTheory.Limits.walkingSpanOpEquiv.functor.map f =
    (CategoryTheory.Limits.widePushoutShapeOpMap CategoryTheory.Limits.WalkingPair (Opposite.unop Y) (Opposite.unop X)
        f.unop).unop
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.compl_loops_eq : ∀ {α : Type u_1} (M : Matroid α), M.E \ M.loops = {e | M.IsNonloop e}
-- Lean.Elab.PreDefinition.Structural.FindRecArg
Lean.Elab.Structural.prettyRecArg : Array Lean.Expr → Lean.Expr → Lean.Elab.Structural.RecArgInfo → Lean.MetaM Lean.MessageData
-- Mathlib.Order.Lattice
/-- The infimum is the *greatest* lower bound  -/
Lattice.le_inf : ∀ {α : Type u} [self : Lattice α] (a b c : α), a ≤ b → a ≤ c → a ≤ Lattice.inf b c
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
/-- A finite measure `μ` over `(Π i, X i) × (Π j, Y j)` is determined by the values
`∫⁻ p, (Π i, f i (p.1 i)) * (Π j, g j (p.2 j)) ∂μ`, for `f : (i : ι) → X i → ℝ≥0`
and `g : (j : κ) → Y j → ℝ≥0` any families of bounded continuous functions.  -/
Measure.ext_of_lintegral_prod_mul_prod_boundedContinuousFunction : ∀ {ι : Type u_1} {κ : Type u_2} {X : ι → Type u_5} {Y : κ → Type u_6} {mX : (i : ι) → MeasurableSpace (X i)}
  [inst : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), BorelSpace (X i)] [∀ (i : ι), HasOuterApproxClosed (X i)]
  {mY : (j : κ) → MeasurableSpace (Y j)} [inst_3 : (j : κ) → TopologicalSpace (Y j)] [∀ (j : κ), BorelSpace (Y j)]
  [∀ (j : κ), HasOuterApproxClosed (Y j)] [inst_6 : Fintype ι] [inst_7 : Fintype κ]
  {μ ν : MeasureTheory.Measure (((i : ι) → X i) × ((j : κ) → Y j))} [MeasureTheory.IsFiniteMeasure μ],
  (∀ (f : (i : ι) → BoundedContinuousFunction (X i) NNReal) (g : (j : κ) → BoundedContinuousFunction (Y j) NNReal),
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑(∏ i, (f i) (p.1 i)) * ↑(∏ j, (g j) (p.2 j)) ∂μ =
        ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑(∏ i, (f i) (p.1 i)) * ↑(∏ j, (g j) (p.2 j)) ∂ν) →
    μ = ν
-- Aesop.Tree.Data
Aesop.Goal.setSuccessProbability : Aesop.Percent → Aesop.Goal → Aesop.Goal
-- Mathlib.Order.Interval.Set.Fin
Fin.image_succ_uIoc : ∀ {n : ℕ} (i j : Fin n), Fin.succ '' Set.uIoc i j = Set.uIoc i.succ j.succ
-- Init.Data.List.Lemmas
List.length_flatten : ∀ {α : Type u_1} {L : List (List α)}, L.flatten.length = (List.map List.length L).sum
-- Mathlib.Logic.Basic
And.exists : ∀ {p q : Prop} {f : p ∧ q → Prop}, (∃ (h : p ∧ q), f h) ↔ ∃ (hp : p) (hq : q), f ⋯
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.RightResolution.comp_f_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  {R R' R'' : Φ.RightResolution X₂} (φ : R ⟶ R') (ψ : R' ⟶ R'') {Z : C₁} (h : R''.X₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp φ ψ).f h =
    CategoryTheory.CategoryStruct.comp φ.f (CategoryTheory.CategoryStruct.comp ψ.f h)
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
one_lt_mabs : ∀ {α : Type u_1} [inst : Group α] [inst_1 : LinearOrder α] [MulLeftMono α] {a : α}, 1 < |a|ₘ ↔ a ≠ 1
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- Natural isomorphisms between functors lift to additive group objects.  -/
CategoryTheory.Functor.mapAddGrpNatIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            {F F' : CategoryTheory.Functor C D} →
              [inst_4 : F.Monoidal] → [inst_5 : F'.Monoidal] → (F ≅ F') → (F.mapAddGrp ≅ F'.mapAddGrp)
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestMatchAtChain.le : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice}
  {startPos endPos : s.Pos}, String.Slice.Pattern.Model.IsLongestMatchAtChain pat startPos endPos → startPos ≤ endPos
-- Mathlib.RingTheory.Teichmuller
Perfection.teichmuller₀_spec' : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommRing R] {I : Ideal R} [inst_2 : CharP (R ⧸ I) p]
  [inst_3 : IsAdicComplete I R] {x : Perfection (R ⧸ I) p} {y : R},
  (∃ N, ∀ n ≥ N, ∃ z, (Ideal.Quotient.mk I) z = (Perfection.coeff (R ⧸ I) p n) x ∧ z ^ p ^ n ≡ y [SMOD I ^ (n + 1)]) →
    (Perfection.teichmuller₀ p I) x = y
-- Mathlib.LinearAlgebra.Projectivization.Cardinality
Projectivization.card_of_finrank : ∀ (k : Type u_1) (V : Type u_2) [inst : Field k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] [Finite k] {n : ℕ},
  Module.finrank k V = n → Nat.card (Projectivization k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i
-- Mathlib.Topology.MetricSpace.Similarity
/-- A similarity scales non-negative distance. Forward direction of
`similar_iff_exists_nndist_eq`.  -/
Similar.exists_nndist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoMetricSpace P₁]
  [inst_1 : PseudoMetricSpace P₂],
  Similar v₁ v₂ → ∃ r, r ≠ 0 ∧ ∀ (i₁ i₂ : ι), nndist (v₁ i₁) (v₁ i₂) = r * nndist (v₂ i₁) (v₂ i₂)
-- Mathlib.Algebra.Group.End
Equiv.Perm.equivUnitsEnd_symm_apply_symm_apply : ∀ {α : Type u_4} (u : (Function.End α)ˣ), ⇑(Equiv.symm (Equiv.Perm.equivUnitsEnd.symm u)) = ↑u⁻¹
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.opLaxMonoidalPi' : {I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] →
        {D : Type u_1} →
          [inst_2 : CategoryTheory.Category.{v_1, u_1} D] →
            [inst_3 : CategoryTheory.MonoidalCategory D] →
              (F : (i : I) → CategoryTheory.Functor D (C i)) →
                [(i : I) → (F i).OplaxMonoidal] → (CategoryTheory.Functor.pi' F).OplaxMonoidal
-- Mathlib.Algebra.Lie.Weights.Cartan
LieAlgebra.mem_biSup_genWeightSpace_of : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  {H : LieSubalgebra R L} [inst_3 : LieRing.IsNilpotent ↥H] {M : Type u_3} [inst_4 : AddCommGroup M]
  [inst_5 : Module R M] [inst_6 : LieRingModule L M] [inst_7 : LieModule R L M] {s : Set (↥H → R)},
  (∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s) →
    ∀ {x : L} {m : M},
      x ∈ ⨆ χ ∈ s, LieAlgebra.rootSpace H χ →
        m ∈ ⨆ χ ∈ s, LieModule.genWeightSpace M χ → ⁅x, m⁆ ∈ ⨆ χ ∈ s, LieModule.genWeightSpace M χ
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.support_comap_subset : ∀ {V : Type u_1} {W : Type u_2} (f : V → W) (G : SimpleGraph W), (SimpleGraph.comap f G).support ⊆ f ⁻¹' G.support
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.ofCLM_surjective : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F],
  Function.Surjective ContinuousLinearMapWOT.ofCLM
-- Mathlib.Computability.EpsilonNFA
/-- Transition function. The automaton is rendered non-deterministic by this transition function
returning `Set σ` (rather than `σ`), and ε-transitions are made possible by taking `Option α`
(rather than `α`).  -/
εNFA.step : {α : Type u} → {σ : Type v} → εNFA α σ → σ → Option α → Set σ
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.HasModel.instRxcHasSize.eq_1 : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] {β : Type v} [inst_2 : LE β] [inst_3 : LT β]
  [inst_4 : Std.PRange.UpwardEnumerable β] [inst_5 : Std.PRange.LawfulUpwardEnumerable β]
  [inst_6 : Std.PRange.LawfulUpwardEnumerableLE β] [inst_7 : Std.PRange.LawfulUpwardEnumerableLT β] [m : HasModel✝ α β]
  [inst_8 : Std.Rxc.HasSize β],
  HasModel.instRxcHasSize✝ = { size := fun lo hi => Std.Rxc.HasSize.size (HasModel.encode✝ lo) (HasModel.encode✝ hi) }
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.hasProducts_shrink : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C],
  CategoryTheory.Limits.HasProducts C
-- Lean.Meta.Tactic.Repeat
/-- Auxiliary for `repeat'Core`. `repeat'Core.go f maxIters progress goals stk acc` evaluates to
essentially `acc.toList ++ repeat' f (goals::stk).join maxIters`: that is, `acc` are goals we will
not revisit, and `(goals::stk).join` is the accumulated todo list of subgoals.  -/
_private.Lean.Meta.Tactic.Repeat.0.Lean.Meta.repeat'Core.go : {m : Type → Type} →
  {ε : Type u_1} →
    {s : Type} →
      [Monad m] →
        [MonadExcept ε m] →
          [Lean.MonadBacktrack s m] →
            [Lean.MonadMCtx m] →
              (Lean.MVarId → m (List Lean.MVarId)) →
                ℕ → Bool → List Lean.MVarId → List (List Lean.MVarId) → Array Lean.MVarId → m (Bool × Array Lean.MVarId)
-- Mathlib.RingTheory.Perfection
PreTilt.valAux.congr_simp : ∀ (K : Type u₁) [inst : Field K] (v v_1 : Valuation K NNReal),
  v = v_1 →
    ∀ (O : Type u₂) [inst_1 : CommRing O] [inst_2 : Algebra O K] (p : ℕ) [inst_3 : Fact (Nat.Prime p)]
      [inst_4 : Fact ¬IsUnit ↑p] (f f_1 : PreTilt O p),
      f = f_1 → PreTilt.valAux K v O p f = PreTilt.valAux K v_1 O p f_1
-- Mathlib.Logic.Relation
Relation.instTransTransGenReflTransGen : {α : Type u_1} → {r : α → α → Prop} → Trans (Relation.TransGen r) (Relation.ReflTransGen r) (Relation.TransGen r)
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.isCompleteBetween_comm : ∀ {V : Type u} (G : SimpleGraph V) {s t : Set V}, G.IsCompleteBetween s t ↔ G.IsCompleteBetween t s
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.Colorable.chromaticNumber_le : ∀ {V : Type u} {G : SimpleGraph V} {n : ℕ}, G.Colorable n → G.chromaticNumber ≤ ↑n
-- Mathlib.Data.Nat.Digits.Div
Nat.nine_dvd_iff : ∀ (n : ℕ), 9 ∣ n ↔ 9 ∣ (Nat.digits 10 n).sum
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
/-- If two morphisms in `Arrow V` are right homotopic, then they become equal in the right
Freyd category.  -/
CategoryTheory.Preadditive.RightFreyd.eq_of_rightHomotopy : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v : CategoryTheory.Arrow V} (f g : u ⟶ v) (h : CategoryTheory.Arrow.RightHomotopy f g),
  (CategoryTheory.Preadditive.RightFreyd.quotient V).map f = (CategoryTheory.Preadditive.RightFreyd.quotient V).map g
-- Init.Grind.Lemmas
Lean.Grind.beq_eq_false_of_diseq : ∀ {α : Type u} {x : BEq α} {x_1 : LawfulBEq α} {a b : α}, ¬a = b → (a == b) = false
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.ae_ae_of_ae_compProd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ]
  {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η] {a : α} {p : β × γ → Prop},
  (∀ᵐ (bc : β × γ) ∂(κ.compProd η) a, p bc) → ∀ᵐ (b : β) ∂κ a, ∀ᵐ (c : γ) ∂η (a, b), p (b, c)
-- Mathlib.RingTheory.TensorProduct.DirectLimitFG
TensorProduct.eq_of_fg_of_subtype_eq' : ∀ {R : Type u} {M : Type u_1} {N : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {P : Submodule R M},
  P.FG →
    ∀ {t : TensorProduct R (↥P) N} {P' : Submodule R M},
      P'.FG →
        ∀ {t' : TensorProduct R (↥P') N},
          (LinearMap.rTensor N P.subtype) t = (LinearMap.rTensor N P'.subtype) t' →
            ∃ Q,
              ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q),
                Q.FG ∧
                  (LinearMap.rTensor N (Submodule.inclusion hPQ)) t =
                    (LinearMap.rTensor N (Submodule.inclusion hP'Q)) t'
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.sSup_le_sSup_add_one : ∀ (s : Set Ordinal.{u_3}), sSup s ≤ sSup ((fun x => x + 1) '' s)
-- Mathlib.RingTheory.PowerSeries.Trunc
PowerSeries.trunc_trunc_of_le : ∀ {R : Type u_2} [inst : CommSemiring R] {n m : ℕ} (f : PowerSeries R),
  autoParam (n ≤ m) PowerSeries.trunc_trunc_of_le._auto_1 →
    (PowerSeries.trunc n) ↑((PowerSeries.trunc m) f) = (PowerSeries.trunc n) f
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.openAlgebra : (R : Type u) →
  [inst : CommRing R] →
    (U : (TopologicalSpace.Opens (PrimeSpectrum R))ᵒᵖ) →
      Algebra R ↑((AlgebraicGeometry.Spec.structureSheaf R).obj.obj U)
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.mem_iSup_of_directed : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {ι : Type u_3} [hι : Nonempty ι]
  {S : ι → L.Substructure M}, Directed (fun x1 x2 => x1 ≤ x2) S → ∀ {x : M}, x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i
-- Mathlib.Order.OmegaCompletePartialOrder
_private.Mathlib.Order.OmegaCompletePartialOrder.0.OmegaCompletePartialOrder.Chain.pair.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (x : ℕ) → motive x),
  (match 0 with
    | 0 => h_1 ()
    | x => h_2 x) =
    h_1 ()
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
/-- The natural transformation `F ⊠ G ⟶ (tensor C) ⋙ (G ⊛ F)` that corepresents
the braiding morphism `F ⊛ G ⟶ G ⊛ F`.  -/
CategoryTheory.MonoidalCategory.DayConvolution.braidingHomCorepresenting : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [CategoryTheory.BraidedCategory C] →
            [inst_4 : CategoryTheory.MonoidalCategory V] →
              [CategoryTheory.BraidedCategory V] →
                (F G : CategoryTheory.Functor C V) →
                  [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution G F] →
                    CategoryTheory.MonoidalCategory.externalProduct F G ⟶
                      (CategoryTheory.MonoidalCategory.tensor C).comp
                        (CategoryTheory.MonoidalCategory.DayConvolution.convolution G F)
-- Mathlib.CategoryTheory.Abelian.CommSq
CategoryTheory.CommSq.shortComplex.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X₁ X₂ X₃ X₄ : C}
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] {f f_1 : X₁ ⟶ X₂} (e_f : f = f_1) {g g_1 : X₁ ⟶ X₃}
  (e_g : g = g_1) {inl inl_1 : X₂ ⟶ X₄} (e_inl : inl = inl_1) {inr inr_1 : X₃ ⟶ X₄} (e_inr : inr = inr_1)
  (sq : CategoryTheory.CommSq f g inl inr), sq.shortComplex = ⋯.shortComplex
-- Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap
ContinuousLinearMap.measurable_comp : ∀ {α : Type u_1} [inst : MeasurableSpace α] {R : Type u_2} {E : Type u_3} {F : Type u_4} [inst_1 : Semiring R]
  [inst_2 : SeminormedAddCommGroup E] [inst_3 : Module R E] [inst_4 : MeasurableSpace E] [OpensMeasurableSpace E]
  [inst_6 : SeminormedAddCommGroup F] [inst_7 : Module R F] [inst_8 : MeasurableSpace F] [BorelSpace F] (L : E →L[R] F)
  {φ : α → E}, Measurable φ → Measurable fun a => L (φ a)
-- Mathlib.Topology.Category.CompHaus.EffectiveEpi
CompHaus.effectiveEpiFamily_of_jointly_surjective : ∀ {α : Type} [Finite α] {B : CompHaus} (X : α → CompHaus) (π : (a : α) → X a ⟶ B),
  (∀ (b : ↑B.toTop), ∃ a x, (CategoryTheory.ConcreteCategory.hom (π a)) x = b) → CategoryTheory.EffectiveEpiFamily X π
-- Mathlib.Algebra.Group.Action.Prod
Prod.isScalarTower : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [inst : SMul M α] [inst_1 : SMul M β] [inst_2 : SMul N α]
  [inst_3 : SMul N β] [inst_4 : SMul M N] [IsScalarTower M N α] [IsScalarTower M N β], IsScalarTower M N (α × β)
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_allOnes : ∀ {v i : ℕ}, (BitVec.allOnes v).getMsbD i = decide (i < v)
-- Init.Data.Array.Lemmas
Array.singleton_def : ∀ {α : Type u_1} {v : α}, Array.singleton v = #[v]
-- Mathlib.Tactic.ClickSuggestions.Rewrite
Mathlib.Tactic.ClickSuggestions.RwKey.mk.injEq : ∀ (numGoals : ℕ) (symm : Bool) (nameLength replacementSize : ℕ) (name : String)
  (replacement : Lean.Meta.AbstractMVarsResult) (numGoals_1 : ℕ) (symm_1 : Bool) (nameLength_1 replacementSize_1 : ℕ)
  (name_1 : String) (replacement_1 : Lean.Meta.AbstractMVarsResult),
  ({ numGoals := numGoals, symm := symm, nameLength := nameLength, replacementSize := replacementSize, name := name,
        replacement := replacement } =
      { numGoals := numGoals_1, symm := symm_1, nameLength := nameLength_1, replacementSize := replacementSize_1,
        name := name_1, replacement := replacement_1 }) =
    (numGoals = numGoals_1 ∧
      symm = symm_1 ∧
        nameLength = nameLength_1 ∧ replacementSize = replacementSize_1 ∧ name = name_1 ∧ replacement = replacement_1)
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.norm_mk_le : ∀ {α : Type u_1} {L₁ : List (α × Bool)} [inst : DecidableEq α], (FreeGroup.mk L₁).norm ≤ L₁.length
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.swapAt_eq_swapAtTR.go : ∀ (α : Type u_1) (v : α) (xs : List α) (i : ℕ) (acc : Array α),
  List.swapAtTR.go (acc.toList ++ xs) v xs i acc = (xs[i]?.getD v, acc.toList ++ xs.set i v)
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.toVal.injEq : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  (ofVal ofVal_1 : R), (WithVal.toVal v ofVal = WithVal.toVal v ofVal_1) = (ofVal = ofVal_1)
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.InductionCandidate.val : Lean.Meta.Try.Collector.InductionCandidate → Lean.InductiveVal
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.add_eq_sup : ∀ {X : AlgebraicGeometry.Scheme} (I J : X.IdealSheafData), I + J = I ⊔ J
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.cycleType_eq : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ : Equiv.Perm α} (l : List (Equiv.Perm α)),
  l.prod = σ →
    (∀ σ ∈ l, σ.IsCycle) →
      List.Pairwise Equiv.Perm.Disjoint l → σ.cycleType = ↑(List.map (Finset.card ∘ Equiv.Perm.support) l)
-- Mathlib.RepresentationTheory.Homological.FiniteCyclic
Rep.norm.eq_1 : ∀ {k : Type u} [inst : Semiring k] {G : Type v} [inst_1 : Group G] [inst_2 : Fintype G] (A : Rep.{w, u, v} k G),
  A.norm = Rep.ofHom { toLinearMap := A.ρ.norm, isIntertwining' := ⋯ }
-- Mathlib.Topology.MetricSpace.ProperSpace
instProperSpaceMultiplicative : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] [ProperSpace X], ProperSpace (Multiplicative X)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
/-- the left adjoint  -/
CategoryTheory.Bicategory.Adj.Hom.l : {B : Type u} → [inst : CategoryTheory.Bicategory B] → {a b : B} → CategoryTheory.Bicategory.Adj.Hom a b → (a ⟶ b)
-- Mathlib.Data.Nat.Factorization.Defs
Nat.factorization_minFac_ne_zero : ∀ {n : ℕ}, 1 < n → n.factorization n.minFac ≠ 0
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.fixingSubgroupInsertEquiv.eq_1 : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] (a : α)
  (s : Set ↥(SubMulAction.ofStabilizer M a)),
  SubMulAction.fixingSubgroupInsertEquiv a s =
    { toFun := fun m => ⟨⟨↑m, ⋯⟩, ⋯⟩, invFun := fun m => ⟨↑↑m, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
-- Mathlib.Analysis.Convex.Star
starConvex_zero_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [AddRightMono 𝕜] [inst_3 : AddCommMonoid E]
  [inst_4 : SMulWithZero 𝕜 E] {s : Set E}, StarConvex 𝕜 0 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
-- Mathlib.Order.SuccPred.Basic
/-- A constructor for `PredOrder α` for `α` a linear order.  -/
PredOrder.ofCore : {α : Type u_1} →
  [inst : LinearOrder α] →
    (pred : α → α) →
      (∀ {a : α}, ¬IsMin a → ∀ (b : α), b < a ↔ b ≤ pred a) → (∀ (a : α), IsMin a → pred a = a) → PredOrder α
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.Functor.IsEventuallyConstantTo.isoMap_hom_inv_id : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {F : CategoryTheory.Functor J C} {i₀ : J}
  (h : F.IsEventuallyConstantTo i₀) {i j : J} (φ : i ⟶ j) (hφ : Nonempty (j ⟶ i₀)),
  CategoryTheory.CategoryStruct.comp (F.map φ) (h.isoMap φ hφ).inv = CategoryTheory.CategoryStruct.id (F.obj i)
-- Aesop.Tree.RunMetaM
_private.Aesop.Tree.RunMetaM.0.Aesop.withSaveState : {m : Type → Type u_1} → [Monad m] → [MonadLiftT Lean.MetaM m] → {α : Type} → m α → m (α × Lean.Meta.SavedState)
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
/-- The value `BoxIntegral.IntegrationParams.GP = ⊥`
(`bRiemann = false`, `bHenstock = true`, `bDistortion = true`)
corresponds to a generalization of the Henstock integral such that the Divergence theorem holds true
without additional integrability assumptions, see the module docstring for details.  -/
BoxIntegral.IntegrationParams.instInhabited : Inhabited BoxIntegral.IntegrationParams
-- Mathlib.RingTheory.Finiteness.Defs
Submodule.fg_iff_exists_finite_generating_family : ∀ {A : Type u} [inst : Semiring A] {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module A M] {N : Submodule A M},
  N.FG ↔ ∃ G, ∃ (_ : Finite G), ∃ g, Submodule.span A (Set.range g) = N
-- Mathlib.FieldTheory.PurelyInseparable.Basic
instUniqueAlgHomOfIsPurelyInseparable : (F : Type u) →
  (E : Type v) →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          [IsPurelyInseparable F E] →
            (L : Type w) →
              [inst_4 : CommRing L] →
                [IsReduced L] →
                  [inst_6 : Algebra F L] → [inst_7 : Algebra E L] → [IsScalarTower F E L] → Unique (E →ₐ[F] L)
-- Std.Time.DateTime.PlainDateTime
/-- Converts a `WallTime` to a `PlainTime`.
 -/
Std.Time.PlainTime.ofWallTime : Std.Time.WallTime → Std.Time.PlainTime
-- Init.Data.UInt.Bitwise
UInt64.toUSize_and : ∀ (a b : UInt64), (a &&& b).toUSize = a.toUSize &&& b.toUSize
-- Init.Data.Vector.Algebra
Vector.instSMul : {α : Type u_1} → {β : Type u_2} → {n : ℕ} → [SMul α β] → SMul α (Vector β n)
-- Mathlib.Algebra.Algebra.Operations
Submodule.instNoZeroDivisors : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [NoZeroDivisors A], NoZeroDivisors (Submodule R A)
-- Mathlib.ModelTheory.ElementaryMaps
/-- A first-order equivalence is also an elementary embedding.  -/
FirstOrder.Language.Equiv.toElementaryEmbedding : {L : FirstOrder.Language} →
  {M : Type u_1} →
    {N : Type u_2} → [inst : L.Structure M] → [inst_1 : L.Structure N] → L.Equiv M N → L.ElementaryEmbedding M N