mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.gaussianReal_neg : ∀ {μ : ℝ} {v : NNReal} {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : Ω → ℝ},
  ProbabilityTheory.HasLaw X (ProbabilityTheory.gaussianReal μ v) P →
    ProbabilityTheory.HasLaw (-X) (ProbabilityTheory.gaussianReal (-μ) v) P
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
OrdinalApprox.gfpApprox_of_isSuccLimit : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α} {a : Ordinal.{u}},
  Order.IsSuccLimit a → OrdinalApprox.gfpApprox f x a = ⨅ b, OrdinalApprox.gfpApprox f x ↑b
-- Init.Internal.Order.Basic
Lean.Order.coind_monotone_exists : ∀ {α : Sort u_1} [inst : Lean.Order.PartialOrder α] {β : Sort u_2} (f : α → β → Lean.Order.ReverseImplicationOrder),
  Lean.Order.monotone f → Lean.Order.monotone fun x => Exists (f x)
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.instMulEquivClass : ∀ {A : Type u_2} {B : Type u_3} [inst : Mul A] [inst_1 : Mul B] [inst_2 : Star A] [inst_3 : Star B],
  MulEquivClass (A ≃⋆* B) A B
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.lt_zpow_iff_log_lt : ∀ {x y : ℝ} {n : ℤ}, 0 < x → 0 < y → (x < y ^ n ↔ Real.log x < ↑n * Real.log y)
-- Mathlib.CategoryTheory.Triangulated.TStructure.Heart
CategoryTheory.Triangulated.TStructure.Heart.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              {t : CategoryTheory.Triangulated.TStructure C} →
                {H : Type u'} →
                  [inst_6 : CategoryTheory.Category.{v', u'} H] →
                    [inst_7 : CategoryTheory.Preadditive H] →
                      (ι : CategoryTheory.Functor H C) →
                        autoParam ι.Additive CategoryTheory.Triangulated.TStructure.Heart.additive_ι._autoParam →
                          autoParam ι.Full CategoryTheory.Triangulated.TStructure.Heart.full_ι._autoParam →
                            autoParam ι.Faithful CategoryTheory.Triangulated.TStructure.Heart.faithful_ι._autoParam →
                              autoParam (ι.essImage = t.heart)
                                  CategoryTheory.Triangulated.TStructure.Heart.essImage_eq_heart._autoParam →
                                t.Heart H
-- Lean.Environment
Lean.EnvExtension.mkInitialExtStates : IO (Array Lean.EnvExtensionState)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.congr_arg : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) {x y : P1}, x = y → f x = f y
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey?_le_maxKey?_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β} {km kmi : α}, t.maxKey? = some km → (t.insertIfNew k v).maxKey?.get ⋯ = kmi → (cmp km kmi).isLE = true
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.induce_cons : ∀ {V : Type u} {G : SimpleGraph V} {u v u' : V} {s : Set V} (huu' : G.Adj u u') (w : G.Walk u' v)
  (hw : ∀ x ∈ (SimpleGraph.Walk.cons huu' w).support, x ∈ s),
  SimpleGraph.Walk.induce s (SimpleGraph.Walk.cons huu' w) hw = SimpleGraph.Walk.cons ⋯ (SimpleGraph.Walk.induce s w ⋯)
-- Mathlib.MeasureTheory.Function.FactorsThrough
/-- If a function `g` is measurable with respect to the pullback along some function `f`,
then to prove `g x = g y` it is enough to prove `f x = f y`.  -/
Measurable.factorsThrough : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [mY : MeasurableSpace Y] {f : X → Y} {g : X → Z}
  [inst : MeasurableSpace Z] [MeasurableSingletonClass Z], Measurable g → Function.FactorsThrough g f
-- Lean.Expr
Lean.ExprSet : Type
-- Mathlib.Data.Set.Image
Set.range_eq_empty : ∀ {α : Type u_1} {ι : Sort u_4} [IsEmpty ι] (f : ι → α), Set.range f = ∅
-- Mathlib.Data.Set.Function
Set.RightInvOn.eq : ∀ {α : Type u_1} {β : Type u_2} {t : Set β} {f : α → β} {f' : β → α},
  Set.RightInvOn f' f t → ∀ {y : β}, y ∈ t → f (f' y) = y
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.instIsIsoRightAppArrowMapToTypeOrdFunctorIterationFunctor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ]
  {j₁ j₂ : κ.ord.ToType} (φ : j₁ ⟶ j₂) (f : CategoryTheory.Arrow C),
  CategoryTheory.IsIso
    (CategoryTheory.Arrow.Hom.right (((CategoryTheory.SmallObject.iterationFunctor I κ).map φ).app f))
-- Mathlib.Algebra.Star.Basic
star_mem_iff : ∀ {R : Type u} {S : Type u_1} [inst : SetLike S R] [inst_1 : InvolutiveStar R] [StarMemClass S R] {s : S} {x : R},
  star x ∈ s ↔ x ∈ s
-- Mathlib.Analysis.Real.Sqrt
Real.lt_sq_of_sqrt_lt : ∀ {x y : ℝ}, √x < y → x < y ^ 2
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.isoApp_hom : ∀ {I : Type w₀} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {X Y : (i : I) → C i}
  (f : X ≅ Y) (i : I), (CategoryTheory.Pi.isoApp f i).hom = f.hom i
-- Mathlib.Data.Nat.Factorization.Basic
Nat.ordCompl_dvd : ∀ (n p : ℕ), n / p ^ n.factorization p ∣ n
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- An analogue of `Filter.HasBasis.tendsto_iff` for `TendstoUniformlyOnFilter`.  -/
Filter.HasBasis.tendstoUniformlyOnFilter_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β] {X : Type u_5} {ιX : Type u_6} {ια : Type u_7} {ιβ : Type u_8}
  {F : X → α → β} {f : α → β} {l : Filter X} {l' : Filter α} {pX : ιX → Prop} {sX : ιX → Set X} {pα : ια → Prop}
  {sα : ια → Set α} {pβ : ιβ → Prop} {sβ : ιβ → Set (β × β)},
  l.HasBasis pX sX →
    l'.HasBasis pα sα →
      (uniformity β).HasBasis pβ sβ →
        (TendstoUniformlyOnFilter F f l l' ↔
          ∀ (i : ιβ), pβ i → ∃ j k, (pX j ∧ pα k) ∧ ∀ (x : X) (a : α), x ∈ sX j → a ∈ sα k → (f a, F x a) ∈ sβ i)
-- Lean.Data.JsonRpc
Lean.JsonRpc.ResponseError.ofMessage? : Lean.JsonRpc.Message → Option (Lean.JsonRpc.ResponseError Lean.Json)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
SimplexCategoryGenRel.δ_comp_σ_of_gt_assoc : ∀ {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)},
  j.castSucc < i →
    ∀ {Z : SimplexCategoryGenRel} (h : SimplexCategoryGenRel.mk (n + 1) ⟶ Z),
      CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.δ i.succ)
          (CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.σ j.castSucc) h) =
        CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.σ j)
          (CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.δ i) h)
-- Mathlib.Algebra.Polynomial.Eval.Defs
/-- The composition of polynomials as a polynomial.  -/
Polynomial.comp : {R : Type u} → [inst : Semiring R] → Polynomial R → Polynomial R → Polynomial R
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.str : (self : GrpCat) → Group ↑self
-- Std.Time.Format.Modifier
Std.Time.Modifier.K.sizeOf_spec : ∀ (presentation : Std.Time.Number), sizeOf (Std.Time.Modifier.K presentation) = 1 + sizeOf presentation
-- Mathlib.LinearAlgebra.Multilinear.Pi
MultilinearMap.piFamily_zero : ∀ {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN}
  [inst : Semiring R] [inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)]
  [inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)] [inst_3 : (i : ι) → (k : κ i) → Module R (M i k)]
  [inst_4 : (p : (i : ι) → κ i) → Module R (N p)], MultilinearMap.piFamily 0 = 0
-- Mathlib.Algebra.Group.Subgroup.Map
AddEquiv.mapAddSubgroup_symm_apply : ∀ {G : Type u_1} [inst : AddGroup G] {H : Type u_6} [inst_1 : AddGroup H] (f : G ≃+ H) (H_1 : AddSubgroup H),
  (RelIso.symm f.mapAddSubgroup) H_1 = AddSubgroup.map (↑f.symm) H_1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.hasPullbackVertPaste : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (g' : W ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.snd f g) g'],
  CategoryTheory.Limits.HasPullback f (CategoryTheory.CategoryStruct.comp g' g)
-- Mathlib.NumberTheory.NumberField.House
_private.Mathlib.NumberTheory.NumberField.House.0.NumberField.house.house_le_bound : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {α : Type u_2} {β : Type u_3}
  (a : Matrix α β (NumberField.RingOfIntegers K)) {p q : ℕ},
  p < q →
    ∀ (x : β × (K →+* ℂ) → ℤ) [inst_2 : Fintype β] {A : ℝ},
      (∀ (k : α) (l : β), NumberField.house ((algebraMap (NumberField.RingOfIntegers K) K) (a k l)) ≤ A) →
        ∀ [inst_3 : DecidableEq (K →+* ℂ)] [inst_4 : Fintype α],
          0 ≤ A →
            ‖x‖ ≤ (↑q * ↑(Module.finrank ℚ K) * ‖NumberField.house.asiegel✝ K a‖) ^ (↑p / (↑q - ↑p)) →
              ∀ (l : β),
                NumberField.house ↑(NumberField.house.ξ✝ K x l) ≤
                  NumberField.house.c₁✝ K * (NumberField.house.c₁✝ K * ↑q * A) ^ (↑p / (↑q - ↑p))
-- Lean.Meta.Sym.SymM
/-- Instances registered by satellite modules for types they create themselves
(e.g., `grind linarith`'s envelope type `IntModule.OfNatModule.Q`).
`Sym.synthInstance?` consults this table (keyed by the instance type, structural equality)
before running typeclass resolution. This both skips searches whose results are known in
advance, and ensures the registered term is used as the canonical representative.

We currently use this table to reduce the overhead of type class resolution in `grind`.
 -/
Lean.Meta.Sym.State.instanceOverrides : Lean.Meta.Sym.State → Lean.PHashMap Lean.Expr Lean.Expr
-- Lean.Data.FuzzyMatching
/-- Whether characters from the pattern and the word match.  -/
_private.Lean.Data.FuzzyMatching.0.Lean.FuzzyMatching.fuzzyMatchCore.allowMatch : Char → Char → Lean.FuzzyMatching.CharRole → Lean.FuzzyMatching.CharRole → Bool
-- Mathlib.Algebra.Order.Archimedean.Basic
/-- A linear ordered field that is a floor ring is archimedean.  -/
FloorRing.archimedean : ∀ (K : Type u_5) [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [FloorRing K], Archimedean K
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
ChainComplex.of.congr_simp : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  {α : Type u_2} [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α] [inst_4 : DecidableEq α] (X : α → V)
  (d d_1 : (n : α) → X (n + 1) ⟶ X n) (e_d : d = d_1)
  (sq : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d (n + 1)) (d n) = 0),
  ChainComplex.of X d sq = ChainComplex.of X d_1 ⋯
-- Mathlib.Analysis.Fourier.FourierTransform
VectorFourier.fourierIntegral_continuousLinearMap_apply : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} {V : Type u_5} {W : Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : MeasurableSpace V] [BorelSpace V]
  [inst_5 : NormedAddCommGroup W] [inst_6 : NormedSpace 𝕜 W] {e : AddChar 𝕜 Circle} {μ : MeasureTheory.Measure V}
  {L : V →L[𝕜] W →L[𝕜] 𝕜} [inst_7 : NormedAddCommGroup F] [inst_8 : NormedSpace ℝ F] [inst_9 : NormedAddCommGroup E]
  [inst_10 : NormedSpace ℂ E] {f : V → F →L[ℝ] E} {a : F} {w : W},
  Continuous ⇑e →
    MeasureTheory.Integrable f μ →
      (VectorFourier.fourierIntegral e μ (ContinuousLinearMap.toLinearMap₁₂ L) f w) a =
        VectorFourier.fourierIntegral e μ (ContinuousLinearMap.toLinearMap₁₂ L) (fun x => (f x) a) w
-- Mathlib.RingTheory.Smooth.Basic
Algebra.FormallySmooth.localization_base : ∀ {R : Type u_4} {Rₘ : Type u_6} {Sₘ : Type u_7} [inst : CommRing R] [inst_1 : CommRing Rₘ] [inst_2 : CommRing Sₘ]
  (M : Submonoid R) [inst_3 : Algebra R Sₘ] [inst_4 : Algebra R Rₘ] [inst_5 : Algebra Rₘ Sₘ] [IsScalarTower R Rₘ Sₘ]
  [IsLocalization M Rₘ] [Algebra.FormallySmooth R Sₘ], Algebra.FormallySmooth Rₘ Sₘ
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_rev : ∀ {w : ℕ} (x : BitVec w) (i : Fin w), x.getMsbD ↑i.rev = x.getLsbD ↑i
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.isSquare : ∀ (x : ℂ), IsSquare x
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.productMap_left : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : CommSemiring S] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R S]
  (f : A →ₐ[R] S) (g : B →ₐ[R] S), (Algebra.TensorProduct.productMap f g).comp Algebra.TensorProduct.includeLeft = f
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiff.comp₂ : ∀ {𝕜 : Type u_1} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {E₁ : Type u_6}
  {E₂ : Type u_7} [inst_5 : NormedAddCommGroup E₁] [inst_6 : NormedAddCommGroup E₂] [inst_7 : NormedSpace 𝕜 E₁]
  [inst_8 : NormedSpace 𝕜 E₂] {g : E₁ × E₂ → G} {f₁ : F → E₁} {f₂ : F → E₂},
  ContDiff 𝕜 n g → ContDiff 𝕜 n f₁ → ContDiff 𝕜 n f₂ → ContDiff 𝕜 n fun x => g (f₁ x, f₂ x)
-- Mathlib.CategoryTheory.SingleObj
CategoryTheory.SingleObj.id_as_one : ∀ (M : Type u) [inst : Monoid M] (x : CategoryTheory.SingleObj M), CategoryTheory.CategoryStruct.id x = 1
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- A continuous linear equivalence of domains
defines an equivalence between continuous alternating maps.

This is available as a continuous linear isomorphism at
`ContinuousLinearEquiv.continuousAlternatingMapCongrLeft`.

This is `ContinuousAlternatingMap.compContinuousLinearMap` as an equivalence.  -/
ContinuousLinearEquiv.continuousAlternatingMapCongrLeftEquiv : {R : Type u_1} →
  {M : Type u_2} →
    {M' : Type u_3} →
      {N : Type u_4} →
        {ι : Type u_6} →
          [inst : Semiring R] →
            [inst_1 : AddCommMonoid M] →
              [inst_2 : Module R M] →
                [inst_3 : TopologicalSpace M] →
                  [inst_4 : AddCommMonoid M'] →
                    [inst_5 : Module R M'] →
                      [inst_6 : TopologicalSpace M'] →
                        [inst_7 : AddCommMonoid N] →
                          [inst_8 : Module R N] →
                            [inst_9 : TopologicalSpace N] → (M ≃L[R] M') → M [⋀^ι]→L[R] N ≃ M' [⋀^ι]→L[R] N
-- Aesop.Tracing
Aesop.TraceOption.mk : Lean.Name → Lean.Option Bool → Aesop.TraceOption
-- Lean.Elab.Attributes
Lean.Elab.instInhabitedAttribute : Inhabited Lean.Elab.Attribute
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Subring.integralClosure_subring_le_iff : ∀ {A : Type u_2} [inst : CommRing A] {C : Type u_5} [inst_1 : SetLike C A] [inst_2 : SubringClass C A] {S : C}
  {T : Subring A} [IsIntegrallyClosedIn (↥T) A], (integralClosure (↥S) A).toSubring ≤ T ↔ Subring.ofClass S ≤ T
-- Lean.Server.References
/-- Map from each module to all of its references.
The current references in a file worker take precedence over those in .ilean files.
 -/
Lean.Server.References.AllRefsMap : Type
-- Mathlib.Combinatorics.Matroid.Sum
Matroid.disjointSum_comm : ∀ {α : Type u_1} {M N : Matroid α} {h : Disjoint M.E N.E}, M.disjointSum N h = N.disjointSum M ⋯
-- Mathlib.RingTheory.Regular.RegularSequence
Submodule.top_eq_ofList_cons_smul_iff : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (r : R)
  (rs : List R), ⊤ = Ideal.ofList (r :: rs) • ⊤ ↔ ⊤ = Ideal.ofList rs • ⊤
-- Mathlib.Topology.FiberBundle.Trivialization
/-- Coordinate transformation in the fiber induced by a pair of bundle trivializations,
as a homeomorphism.  -/
Bundle.Trivialization.coordChangeHomeomorph : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          {proj : Z → B} →
            [inst_2 : TopologicalSpace Z] →
              (e₁ e₂ : Bundle.Trivialization F proj) → {b : B} → b ∈ e₁.baseSet → b ∈ e₂.baseSet → F ≃ₜ F
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteArchimedeanClass.mem_ballAddSubgroup_iff : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a : M}
  {c : FiniteArchimedeanClass M}, a ∈ c.ballAddSubgroup ↔ ∀ (h : a ≠ 0), c < FiniteArchimedeanClass.mk a h
-- Plausible.Gen
/-- `sized f` constructs a generator that depends on its `size` parameter  -/
Plausible.Gen.sized : {α : Type} → (ℕ → Plausible.Gen α) → Plausible.Gen α
-- Init.Data.String.Iterate
_private.Init.Data.String.Iterate.0.String.Slice.PosIterator.finitenessRelation : {m : Type → Type u_1} → {s : String.Slice} → [inst : Pure m] → Std.Iterators.FinitenessRelation s.PosIterator m
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
/-- We say `C` has strict initial objects if every initial object is strict, i.e. given any morphism
`f : A ⟶ I` where `I` is initial, then `f` is an isomorphism.

Strictly speaking, this says that *any* initial object must be strict, rather than that strict
initial objects exist.
 -/
CategoryTheory.Limits.HasStrictInitialObjects : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Init.Data.List.Attach
List.attach_ne_nil_iff : ∀ {α : Type u_1} {l : List α}, l.attach ≠ [] ↔ l ≠ []
-- Init.Data.Fin.Lemmas
False.elim.congr_simp : ∀ {C : Sort u} (h : False), h.elim = h.elim
-- Mathlib.Data.Set.Sups
Set.inf_mem_infs : ∀ {α : Type u_2} [inst : SemilatticeInf α] {s t : Set α} {a b : α}, a ∈ s → b ∈ t → a ⊓ b ∈ s ⊼ t
-- Mathlib.Probability.Process.HittingTime
/-- The hitting time of a discrete process with the starting time indexed by a stopping time
is a stopping time.  -/
MeasureTheory.Adapted.isStoppingTime_hittingBtwn_isStoppingTime : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : ConditionallyCompleteLinearOrder ι]
  [WellFoundedLT ι] [Countable ι] [inst_3 : TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι]
  [inst_6 : MeasurableSpace β] {f : MeasureTheory.Filtration ι m} {u : ι → Ω → β} {τ : Ω → WithTop ι},
  MeasureTheory.IsStoppingTime f τ →
    ∀ {N : ι},
      (∀ (x : Ω), τ x ≤ ↑N) →
        ∀ {s : Set β},
          MeasurableSet s →
            MeasureTheory.Adapted f u →
              MeasureTheory.IsStoppingTime f fun x => ↑(MeasureTheory.hittingBtwn u s (τ x).untopA N x)
-- Mathlib.Order.Category.Preord
Preord.coe_id : ∀ {X : Preord}, ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
-- Mathlib.Topology.Closure
closure_inter_of_codisjoint_interior : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X},
  Codisjoint (interior s) (interior t) → closure (s ∩ t) = closure s ∩ closure t
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.IsReflection.not_isRightInversion_mul_left_iff : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {t : W},
  cs.IsReflection t → ∀ {w : W}, ¬cs.IsRightInversion (w * t) t ↔ cs.IsRightInversion w t
-- Mathlib.Order.Basic
LE.le.lt_iff_ne : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, a ≤ b → (a < b ↔ a ≠ b)
-- Aesop.Search.Expansion.Norm
Aesop.normalizeGoalIfNecessary : {Q : Type} → Aesop.GoalRef → [inst : Aesop.Queue Q] → Aesop.SearchM Q Bool
-- Mathlib.Data.Finset.Insert
Finset.insert_val_of_notMem : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Finset α}, a ∉ s → (insert a s).val = a ::ₘ s.val
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.ofNatIso_ι : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂}
  (sq : F.PushoutObjObj f₁ f₂) {F' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} (e : F ≅ F'),
  (sq.ofNatIso e).ι = CategoryTheory.CategoryStruct.comp sq.ι ((e.hom.app Y₁).app Y₂)
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.addSubgroupOf_map_nsmulAddMonoidHom_eq_range : ∀ {M : Type u_6} [inst : AddCommGroup M] (S : AddSubgroup M) (n : ℕ),
  (AddSubgroup.map (nsmulAddMonoidHom n) S).addSubgroupOf S = (nsmulAddMonoidHom n).range
-- Mathlib.CategoryTheory.Abelian.Injective.Ext
CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_add : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.InjectiveResolution Y) {n : ℕ}
  (x y : CochainComplex.HomComplex.CohomologyClass ((CochainComplex.singleFunctor C 0).obj X) R.cochainComplex ↑n),
  R.extEquivCohomologyClass.symm (x + y) = R.extEquivCohomologyClass.symm x + R.extEquivCohomologyClass.symm y
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.equiv_one : ∀ {G : Type u_1} [inst : Group G] {S T : Set G} (hST : Subgroup.IsComplement S T) (hs1 : 1 ∈ S) (ht1 : 1 ∈ T),
  hST.equiv 1 = (⟨1, hs1⟩, ⟨1, ht1⟩)
-- Mathlib.Data.Fin.SuccPred
Fin.castLE_castSucc : ∀ {n m : ℕ} (i : Fin n) (h : n + 1 ≤ m), Fin.castLE h i.castSucc = Fin.castLE ⋯ i
-- Mathlib.RingTheory.PowerSeries.Expand
PowerSeries.expand.congr_simp : ∀ {R : Type u_2} [inst : CommRing R] (p p_1 : ℕ) (e_p : p = p_1) (hp : p ≠ 0),
  PowerSeries.expand p hp = PowerSeries.expand p_1 ⋯
-- Std.Data.DHashMap.Basic
/-- Monadically computes a value by folding the given function over the mappings in the hash
map in some order.
 -/
Std.DHashMap.foldM : {α : Type u} →
  {β : α → Type v} →
    {δ : Type w} →
      {m : Type w → Type w'} →
        [Monad m] → {x : BEq α} → {x_1 : Hashable α} → (δ → (a : α) → β a → m δ) → δ → Std.DHashMap α β → m δ
-- Mathlib.Topology.Algebra.Module.Basic
/-- The span of a separable subset with respect to a separable scalar ring is again separable.  -/
TopologicalSpace.IsSeparable.span : ∀ {R : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : Semiring R] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] [inst_4 : TopologicalSpace R] [TopologicalSpace.SeparableSpace R] [ContinuousAdd M]
  [ContinuousSMul R M] {s : Set M}, TopologicalSpace.IsSeparable s → TopologicalSpace.IsSeparable ↑(Submodule.span R s)
-- Lean.Elab.Exception
Lean.Elab.throwIllFormedSyntax : {m : Type → Type} → {α : Type} → [Monad m] → [Lean.MonadError m] → m α
-- Mathlib.Geometry.Convex.Cone.Face.Basic
PointedCone.isFaceOf_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (F C : PointedCone R M),
  F.IsFaceOf C ↔ F ≤ C ∧ ∀ {x y : M} {a : R}, x ∈ C → y ∈ C → 0 < a → a • x + y ∈ F → x ∈ F
-- Mathlib.Data.Fintype.Basic
Fin.image_succAbove_univ : ∀ {n : ℕ} (i : Fin (n + 1)), Finset.image i.succAbove Finset.univ = {i}ᶜ
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.OpenNhdsOf.instPartialOrder : {α : Type u_2} → [inst : TopologicalSpace α] → {x : α} → PartialOrder (TopologicalSpace.OpenNhdsOf x)
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakKernels
/-- A preadditive category has a weak kernel for `f - g` if it has a weak equalizer
for `f` and `g`.  -/
CategoryTheory.Preadditive.hasWeakKernel_of_hasWeakEqualizer : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  (f g : X ⟶ Y) [CategoryTheory.Limits.HasWeakEqualizer f g], CategoryTheory.Limits.HasWeakKernel (f - g)
-- Init.Data.Int.Bitwise.Lemmas
_private.Init.Data.Int.Bitwise.Lemmas.0.Int.shiftRight.match_1.eq_2 : ∀ (motive : ℤ → ℕ → Sort u_1) (n s : ℕ) (h_1 : (n s : ℕ) → motive (Int.ofNat n) s)
  (h_2 : (n s : ℕ) → motive (Int.negSucc n) s),
  (match Int.negSucc n, s with
    | Int.ofNat n, s => h_1 n s
    | Int.negSucc n, s => h_2 n s) =
    h_2 n s
-- Init.Sym.Lemmas
Lean.Sym.UInt16.eq_eq_false : ∀ (a b : UInt16), decide (a = b) = false → (a = b) = False