mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Set.Prod
Set.pi_inter_compl : ∀ {ι : Type u_1} {α : ι → Type u_2} {t : (i : ι) → Set (α i)} (s : Set ι), s.pi t ∩ sᶜ.pi t = Set.univ.pi t
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.coe_le_coe : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Preorder β] {f g : MeasureTheory.SimpleFunc α β},
  ⇑f ≤ ⇑g ↔ f ≤ g
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.State.tableEntries : Lean.Meta.SynthInstance.State → Std.HashMap Lean.Expr Lean.Meta.SynthInstance.TableEntry
-- Mathlib.RingTheory.Finiteness.Cardinality
/-- If a free module is finite, then any arbitrary basis is finite.  -/
Module.Finite.finite_basis : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial R]
  {ι : Type u_3} [Module.Finite R M] (b : Module.Basis ι R M), Finite ι
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.map_id_id : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N],
  Monoid.Coprod.map (MonoidHom.id M) (MonoidHom.id N) = MonoidHom.id (Monoid.Coprod M N)
-- Mathlib.Analysis.Seminorm
Seminorm.mem_closedBall_self : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E]
  (p : Seminorm 𝕜 E) {x : E} {r : ℝ}, 0 ≤ r → x ∈ p.closedBall x r
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key in the tree map, returning `none` if the
map is empty.
 -/
Std.ExtDTreeMap.Const.minEntry? : {α : Type u} →
  {cmp : α → α → Ordering} → {β : Type v} → [Std.TransCmp cmp] → Std.ExtDTreeMap α (fun x => β) cmp → Option (α × β)
-- Mathlib.MeasureTheory.Measure.Complex
MeasureTheory.ComplexMeasure.equivSignedMeasureₗ_symm_apply : ∀ {α : Type u_1} {m : MeasurableSpace α} {R : Type u_2} [inst : Semiring R] [inst_1 : Module R ℝ]
  [inst_2 : ContinuousConstSMul R ℝ] [inst_3 : ContinuousConstSMul R ℂ]
  (a : MeasureTheory.SignedMeasure α × MeasureTheory.SignedMeasure α),
  MeasureTheory.ComplexMeasure.equivSignedMeasureₗ.symm a = MeasureTheory.ComplexMeasure.equivSignedMeasure.invFun a
-- Mathlib.Order.Partition.Finpartition
/-- The supremum of the partition is `a`  -/
Finpartition.sup_parts : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {a : α} (self : Finpartition a), self.parts.sup id = a
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- the induced map on left homology  -/
CategoryTheory.ShortComplex.LeftHomologyMapData.φH : {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₂} →
          {h₁ : S₁.LeftHomologyData} →
            {h₂ : S₂.LeftHomologyData} → CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂ → (h₁.H ⟶ h₂.H)
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.Ordered.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (t : Std.DTreeMap.Internal.Zipper α β),
  t.Ordered = List.Pairwise (fun a b => compare a.fst b.fst = Ordering.lt) t.toList
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.generate_eq_bot_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (R : CategoryTheory.Presieve X),
  CategoryTheory.Sieve.generate R = ⊥ ↔ R = ⊥
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.weightedHomogeneousComponent_eq_zero' : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] {w : σ → M} (n : M)
  (φ : MvPolynomial σ R),
  (∀ d ∈ φ.support, (Finsupp.weight w) d ≠ n) → (MvPolynomial.weightedHomogeneousComponent w n) φ = 0
-- Mathlib.Algebra.Category.Grp.LeftExactFunctor
_private.Mathlib.Algebra.Category.Grp.LeftExactFunctor.0.AddCommGrpCat.leftExactFunctorForgetEquivalence.instCartesianMonoidalCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasFiniteBiproducts C] → CategoryTheory.CartesianMonoidalCategory C
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- The local frame on `V` induced by a compatible local trivialization `e` of `V` and a basis
`b` of the model fiber `F`. Use `e.localFrame b i` to access the `i`-th section in that frame.

If `x` is outside of `e.baseSet`, this returns the junk value 0.  -/
Bundle.Trivialization.localFrame : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {M : Type u_4} →
      [inst_1 : TopologicalSpace M] →
        {F : Type u_5} →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : NormedSpace 𝕜 F] →
              {V : M → Type u_6} →
                [inst_4 : TopologicalSpace (Bundle.TotalSpace F V)] →
                  [inst_5 : (x : M) → AddCommGroup (V x)] →
                    [inst_6 : (x : M) → Module 𝕜 (V x)] →
                      [inst_7 : (x : M) → TopologicalSpace (V x)] →
                        [inst_8 : FiberBundle F V] →
                          [VectorBundle 𝕜 F V] →
                            {ι : Type u_7} →
                              (e : Bundle.Trivialization F Bundle.TotalSpace.proj) →
                                [MemTrivializationAtlas e] → Module.Basis ι 𝕜 F → ι → (x : M) → V x
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.isStrictValue.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Group.Shrink
equivShrink_symm_mul : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : Mul α] (x y : Shrink.{v, u_2} α),
  (equivShrink α).symm (x * y) = (equivShrink α).symm x * (equivShrink α).symm y
-- Aesop.RuleTac.Cases
_private.Aesop.RuleTac.Cases.0.Aesop.RuleTac.cases.go : Aesop.CasesTarget →
  Lean.Meta.TransparencyMode →
    Bool →
      Array Aesop.CtorNames →
        Lean.MVarId →
          Array Aesop.Subgoal → Array Lean.FVarId → Lean.MVarId → Aesop.ScriptM (Option (Array Aesop.Subgoal))
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.foldRev_eq_foldr_toList : ∀ {α : Type u} {δ : Type w} {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) {f : δ → α → β → δ} {init : δ},
  Std.DHashMap.Raw.Internal.foldRev f init ↑m =
    List.foldr (fun a b => f b a.1 a.2) init (Std.DHashMap.Raw.Const.toList ↑m)
-- Mathlib.Order.CompleteBooleanAlgebra
PUnit.instCompleteBooleanAlgebra : CompleteBooleanAlgebra PUnit.{u_1 + 1}
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.shrinkYonedaCompPresheafFiberIso_inv_app_toPresheafFiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X : C} (x : Φ.fiber.obj X),
  (CategoryTheory.ConcreteCategory.hom (Φ.shrinkYonedaCompPresheafFiberIso.inv.app X)) x =
    (CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiber X x (CategoryTheory.shrinkYoneda.{w, v, u}.obj X)))
      (CategoryTheory.shrinkYonedaObjObjEquiv.symm (CategoryTheory.CategoryStruct.id X))
-- Mathlib.Topology.Algebra.Module.Equiv
/-- Create a `ContinuousLinearEquiv` from two `ContinuousLinearMap`s that are
inverse of each other. See also `equivOfInverse'`.
*ToDo*: Improve the naiming to make it match `LinearMap.ofLinear`.  -/
ContinuousLinearEquiv.equivOfInverse : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R₁] →
      [inst_1 : Semiring R₂] →
        {σ₁₂ : R₁ →+* R₂} →
          {σ₂₁ : R₂ →+* R₁} →
            [inst_2 : RingHomInvPair σ₁₂ σ₂₁] →
              [inst_3 : RingHomInvPair σ₂₁ σ₁₂] →
                {M₁ : Type u_4} →
                  [inst_4 : TopologicalSpace M₁] →
                    [inst_5 : AddCommMonoid M₁] →
                      {M₂ : Type u_5} →
                        [inst_6 : TopologicalSpace M₂] →
                          [inst_7 : AddCommMonoid M₂] →
                            [inst_8 : Module R₁ M₁] →
                              [inst_9 : Module R₂ M₂] →
                                (f₁ : M₁ →SL[σ₁₂] M₂) →
                                  (f₂ : M₂ →SL[σ₂₁] M₁) →
                                    Function.LeftInverse ⇑f₂ ⇑f₁ → Function.RightInverse ⇑f₂ ⇑f₁ → M₁ ≃SL[σ₁₂] M₂
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
HurwitzKernelBounds.isBigO_atTop_F_nat_one : ∀ {a : ℝ}, 0 ≤ a → ∃ p, 0 < p ∧ HurwitzKernelBounds.F_nat 1 a =O[Filter.atTop] fun t => Real.exp (-p * t)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey?_modify : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β),
  (↑m).WF →
    ∀ {k k' : α} {f : β → β},
      (Std.DHashMap.Internal.Raw₀.Const.modify m k f).getKey? k' =
        if (k == k') = true then if m.contains k = true then some k else none else m.getKey? k'
-- Mathlib.ModelTheory.Syntax
_private.Mathlib.ModelTheory.Syntax.0.FirstOrder.Language.Term.constantsToVars.match_1.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u_4} {γ : Type u_2} (motive : (L.withConstants γ).Term α → Sort u_5)
  (f : (L.withConstants γ).Functions 0) (ts : Fin 0 → (L.withConstants γ).Term α)
  (h_1 : (a : α) → motive (FirstOrder.Language.var a))
  (h_2 :
    (f : (L.withConstants γ).Functions 0) →
      (ts : Fin 0 → (L.withConstants γ).Term α) → motive (FirstOrder.Language.func f ts))
  (h_3 :
    (_n : ℕ) →
      (f : (L.withConstants γ).Functions (_n + 1)) →
        (ts : Fin (_n + 1) → (L.withConstants γ).Term α) → motive (FirstOrder.Language.func f ts)),
  (match FirstOrder.Language.func f ts with
    | FirstOrder.Language.var a => h_1 a
    | FirstOrder.Language.func f ts => h_2 f ts
    | FirstOrder.Language.func f ts => h_3 _n f ts) =
    h_2 f ts
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.RelabelNat.State.Inv1.below.insert : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α]
  {motive : (a : ℕ) → (a_1 : Std.HashMap α ℕ) → Std.Sat.AIG.RelabelNat.State.Inv1 a a_1 → Prop} {n : ℕ}
  {map : Std.HashMap α ℕ} {x : α} (hinv : Std.Sat.AIG.RelabelNat.State.Inv1 n map) (hfind : map[x]? = none),
  Std.Sat.AIG.RelabelNat.State.Inv1.below hinv → motive n map hinv → Std.Sat.AIG.RelabelNat.State.Inv1.below ⋯
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.subgraphOfAdj_adj : ∀ {V : Type u} (G : SimpleGraph V) {v w : V} (hvw : G.Adj v w) (a b : V),
  (G.subgraphOfAdj hvw).Adj a b = (s(v, w) = s(a, b))
-- Lean.Meta.Tactic.Simp.SimpCongrTheorems
Lean.Meta.instReprSimpCongrTheorems : Repr Lean.Meta.SimpCongrTheorems
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
/-- The positive and negative parts of a selfadjoint element `a` are unique. That is, if
`a = b - c` is the difference of nonnegative elements whose product is zero, then these are
precisely `a⁺` and `a⁻`.  -/
CFC.posPart_negPart_unique : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [inst_2 : SMulCommClass ℝ A A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : StarRing A] [inst_5 : TopologicalSpace A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A] [StarOrderedRing A]
  [NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] {a b c : A},
  a = b - c →
    b * c = 0 →
      autoParam (0 ≤ b) CFC.posPart_negPart_unique._auto_1 →
        autoParam (0 ≤ c) CFC.posPart_negPart_unique._auto_3 → a⁺ = b ∧ a⁻ = c
-- Mathlib.Data.Finset.Option
Finset.card_insertNone : ∀ {α : Type u_1} (s : Finset α), (Finset.insertNone s).card = s.card + 1
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.refl_comp : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (g : L.Equiv M N), (FirstOrder.Language.Equiv.refl L N).comp g = g
-- Mathlib.Order.CompleteLattice.Lemmas
iInf_ge_eq_iInf_nat_add : ∀ {α : Type u_1} [inst : CompleteLattice α] (u : ℕ → α) (n : ℕ), ⨅ i, ⨅ (_ : i ≥ n), u i = ⨅ i, u (i + n)
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.vietoris.subset_of_specializes : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : Set α} [T1Space α], s ⤳ t → s ⊆ t
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.ext_iff : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s₁ s₂ : AffineSubspace k P), s₁ = s₂ ↔ ↑s₁ = ↑s₂
-- Aesop.Tree.Data
Aesop.GoalData.failedRapps : {Rapp MVarCluster : Type} → Aesop.GoalData Rapp MVarCluster → Array Aesop.RegularRule
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Real.integrableOn_rpowIntegrand₀₁_Ici : ∀ {p x : ℝ},
  p ∈ Set.Ioo 0 1 →
    0 ≤ x → MeasureTheory.IntegrableOn (fun x_1 => p.rpowIntegrand₀₁ x_1 x) (Set.Ici 0) MeasureTheory.volume
-- Mathlib.LinearAlgebra.Dimension.Free
/-- Two vector spaces are isomorphic if they have the same dimension.  -/
nonempty_linearEquiv_of_rank_eq : ∀ {R : Type u} {M M₁ : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  [inst_4 : AddCommMonoid M₁] [inst_5 : Module R M₁] [Module.Free R M₁] [StrongRankCondition R],
  Module.rank R M = Module.rank R M₁ → Nonempty (M ≃ₗ[R] M₁)
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.zsmul_mem : ∀ {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G) {x : G}, x ∈ K → ∀ (n : ℤ), n • x ∈ K
-- Lean.CoreM
Lean.Core.Cache.instLevelType : Lean.Core.Cache → Lean.Core.InstantiateLevelCache
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValNat_factorial_mul_add : ∀ {p n : ℕ} (m : ℕ) [hp : Fact (Nat.Prime p)],
  n < p → padicValNat p (p * m + n).factorial = padicValNat p (p * m).factorial
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.IsCodetector.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : C),
  CategoryTheory.IsCodetector G = (CategoryTheory.ObjectProperty.singleton G).IsCodetecting
-- Mathlib.Topology.Order
isOpen_discrete : ∀ {α : Type u_1} [inst : TopologicalSpace α] [DiscreteTopology α] (s : Set α), IsOpen s
-- Mathlib.SetTheory.ZFC.Rank
ZFSet.rank_powerset : ∀ (x : ZFSet.{u_1}), x.powerset.rank = Order.succ x.rank
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
/-- If `A` is a non-unital `R`-algebra, then the subgroup of units of `Unitization R A` whose
scalar part is `1 : R` (i.e., `Unitization.unitsFstOne`) is isomorphic to the group of units of
`PreQuasiregular A`.  -/
Unitization.unitsFstOne_mulEquiv_quasiregular : (R : Type u_1) →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalSemiring A] →
        [inst_2 : Module R A] →
          [inst_3 : IsScalarTower R A A] →
            [inst_4 : SMulCommClass R A A] → ↥(Unitization.unitsFstOne R A) ≃* (PreQuasiregular A)ˣ
-- Mathlib.Analysis.Meromorphic.Order
/-- At points where a meromorphic function has order zero, the meromorphic order of the logarithmic
derivative is nonnegative.
 -/
meromorphicOrderAt_logDeriv_nonneg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} [CompleteSpace 𝕜] {f : 𝕜 → 𝕜},
  MeromorphicAt f x → meromorphicOrderAt f x = 0 → 0 ≤ meromorphicOrderAt (logDeriv f) x
-- Mathlib.Topology.Algebra.FilterBasis
ModuleFilterBasis.smul : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : TopologicalSpace R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] (B : ModuleFilterBasis R M) {U : Set M}, U ∈ B → ∃ V ∈ nhds 0, ∃ W ∈ B, V • W ⊆ U
-- Mathlib.Algebra.Order.Group.PosPart
negPart_eq_ite_lt : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : AddGroup α] {a : α} [AddLeftMono α], a⁻ = if a < 0 then -a else 0
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α} {k k' : α},
  (k == k') = true →
    k ∉ m → List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (m.insertManyIfNewUnit l).getKey? k' = some k
-- Mathlib.Topology.Algebra.Module.Equiv
/-- Combine a family of linear equivalences into a linear equivalence of `pi`-types.
This is `Equiv.piCongrLeft` as a `ContinuousLinearEquiv`.
 -/
ContinuousLinearEquiv.piCongrLeft : (R : Type u_9) →
  [inst : Semiring R] →
    {ι : Type u_10} →
      {ι' : Type u_11} →
        (φ : ι → Type u_12) →
          [inst_1 : (i : ι) → AddCommMonoid (φ i)] →
            [inst_2 : (i : ι) → Module R (φ i)] →
              [inst_3 : (i : ι) → TopologicalSpace (φ i)] → (e : ι' ≃ ι) → ((i' : ι') → φ (e i')) ≃L[R] (i : ι) → φ i
-- Mathlib.Data.Real.ENatENNReal
ENat.toENNReal_one : ↑1 = 1
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.IsPeriodicPt.of_subsingleton : ∀ {α : Type u_1} [Subsingleton α] (f : α → α) (n : ℕ) (x : α), Function.IsPeriodicPt f n x
-- Init.Data.Nat.Basic
Nat.eq_zero_of_not_pos : ∀ {n : ℕ}, ¬0 < n → n = 0
-- Mathlib.Data.Seq.Parallel
_private.Mathlib.Data.Seq.Parallel.0.Computation.parallel.aux2.match_1.congr_eq_1 : ∀ {α : Type u_1} (motive : α ⊕ List (Computation α) → Sort u_2) (o : α ⊕ List (Computation α))
  (h_1 : (a : α) → motive (Sum.inl a)) (h_2 : (ls : List (Computation α)) → motive (Sum.inr ls)) (a : α),
  o = Sum.inl a →
    (match o with
      | Sum.inl a => h_1 a
      | Sum.inr ls => h_2 ls) ≍
      h_1 a
-- Mathlib.Tactic.Positivity.Basic
/-- Extension for `Nat.gcd`.
Uses positivity of the left term, if available, then tries the right term.

The implementation relies on the fact that `Positivity.core` on `ℕ` never returns `nonzero`.  -/
Mathlib.Meta.Positivity.evalNatGCD : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepSet_iff_Indep : ∀ {Ω : Type u_1} {x : MeasurableSpace Ω} (s t : Set Ω) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.IndepSet s t μ ↔
    ProbabilityTheory.Indep (MeasurableSpace.generateFrom {s}) (MeasurableSpace.generateFrom {t}) μ
-- Init.Internal.Order.Lemmas
Lean.Order.Array.monotone_anyM_loop : ∀ {γ : Type w} [inst : Lean.Order.PartialOrder γ] {m : Type → Type v} [inst_1 : Monad m]
  [inst_2 : (α : Type) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m] {α : Type u} (f : γ → α → m Bool)
  (xs : Array α) (stop : ℕ) (h : stop ≤ xs.size) (j : ℕ),
  Lean.Order.monotone f → Lean.Order.monotone fun x => Array.anyM.loop (f x) xs stop h j
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- Three points are affinely independent if and only if they are not
collinear.  -/
affineIndependent_iff_not_collinear : ∀ {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] {p : Fin 3 → P}, AffineIndependent k p ↔ ¬Collinear k (Set.range p)
-- Mathlib.Order.Disjointed
/-- For any finite family of elements `f : ι → α`, we can find a pairwise-disjoint family `g`
bounded above by `f` and having the same supremum. This is non-canonical, depending on an arbitrary
choice of ordering of `ι`.  -/
Fintype.exists_disjointed_le : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] {ι : Type u_3} [inst_1 : Fintype ι] (f : ι → α),
  ∃ g ≤ f, Finset.univ.sup g = Finset.univ.sup f ∧ Pairwise (Function.onFun Disjoint g)
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.sup' : ∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l l' : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop}
  {s' : ι' → Set α},
  l.HasBasis p s → l'.HasBasis p' s' → (l ⊔ l').HasBasis (fun i => p i.fst ∧ p' i.snd) fun i => s i.fst ∪ s' i.snd
-- Init.SimpLemmas
implies_congr : ∀ {p₁ p₂ : Sort u} {q₁ q₂ : Sort v}, p₁ = p₂ → q₁ = q₂ → (p₁ → q₁) = (p₂ → q₂)
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- The value of `affineCombination`, where the given points are equal.  -/
Finset.affineCombination_apply_const : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : P),
  ∑ i ∈ s, w i = 1 → (Finset.affineCombination k s fun x => p) w = p
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.surjective' : ∀ {X : SSet} {A : X.Subcomplex} (self : A.PairingCore) (x : A.N),
  ∃ s,
    x.toS = { dim := self.dim s + 1, simplex := self.simplex s } ∨
      x.toS =
        { dim := self.dim s,
          simplex :=
            (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X (self.index s)))
              (self.simplex s) }
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.instLattice : {G : Type u_1} → [inst : Group G] → Lattice (FiniteIndexNormalSubgroup G)
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.preΨ'_odd : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R) (m : ℕ),
  W.preΨ' (2 * (m + 2) + 1) =
    (W.preΨ' (m + 4) * W.preΨ' (m + 2) ^ 3 * if Even m then W.Ψ₂Sq ^ 2 else 1) -
      W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3 * if Even m then 1 else W.Ψ₂Sq ^ 2
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.alter!.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (k : α) (f : Option (β k) → Option (β k))
  (size : ℕ) (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.alter! k f (Std.DTreeMap.Internal.Impl.inner size k' v' l' r') =
    match h : compare k k' with
    | Ordering.lt => Std.DTreeMap.Internal.Impl.balance! k' v' (Std.DTreeMap.Internal.Impl.alter! k f l') r'
    | Ordering.gt => Std.DTreeMap.Internal.Impl.balance! k' v' l' (Std.DTreeMap.Internal.Impl.alter! k f r')
    | Ordering.eq =>
      match f (some (cast ⋯ v')) with
      | none => l'.glue! r'
      | some v => Std.DTreeMap.Internal.Impl.inner size k v l' r'
-- Mathlib.NumberTheory.LegendreSymbol.AddCharacter
AddChar.PrimitiveAddChar.mk.inj : ∀ {R : Type u} {inst : CommRing R} {R' : Type v} {inst_1 : Field R'} {n : ℕ+}
  {char : AddChar R (CyclotomicField (↑n) R')} {prim : char.IsPrimitive} {n_1 : ℕ+}
  {char_1 : AddChar R (CyclotomicField (↑n_1) R')} {prim_1 : char_1.IsPrimitive},
  { n := n, char := char, prim := prim } = { n := n_1, char := char_1, prim := prim_1 } → n = n_1 ∧ char ≍ char_1
-- Batteries.Data.Array.Scan
Array.scanr_empty : ∀ {α : Type u_1} {β : Type u_2} {f : α → β → β} {init : β}, Array.scanr f init #[] = #[init]
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The underlying lean expression of a 2-morphism.  -/
Mathlib.Tactic.BicategoryLike.Mor₂.e : Mathlib.Tactic.BicategoryLike.Mor₂ → Lean.Expr
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Complex.range_cos : Set.range Complex.cos = Set.univ
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.Int64.beq_eq_decide_eq : ∀ {a b : Int64}, (a == b) = decide (a = b)
-- Aesop.Tree.TreeM
Aesop.getRootMVarId : Aesop.TreeM Lean.MVarId
-- Init.Data.List.MinMaxOn
List.apply_maxOn_le_iff : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {xs : List α}
  {f : α → β} (h : xs ≠ []) {b : β}, f (List.maxOn f xs h) ≤ b ↔ ∀ x ∈ xs, f x ≤ b
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_eq_keys_contains : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a : α},
  Std.Internal.List.containsKey a l = (Std.Internal.List.keys l).contains a
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
Char.reduceIsWhitespace : Lean.Meta.Simp.DSimproc
-- Mathlib.Order.Minimal
/-- **Alias** of `OrderIso.setOfPredMaximalIsoSetOfPredMinimal`.

---

If two sets are antitonically order isomorphic, their maximals/minimals are too.  -/
OrderIso.setOfMaximalIsoSetOfMinimal : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        {s : Set α} →
          {t : Set β} →
            ↑s ≃o (↑t)ᵒᵈ → ↑{x | Maximal (fun x => x ∈ s) x} ≃o ↑{x | Minimal (fun x => x ∈ t) (OrderDual.ofDual x)}
-- Mathlib.Topology.Homeomorph.Lemmas
Fin.appendHomeomorph_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] (m n : ℕ) (fg : (Fin m → X) × (Fin n → X)) (a : Fin (m + n)),
  (Fin.appendHomeomorph m n) fg a = Fin.append fg.1 fg.2 a
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_of_mem_union_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, k ∈ m₁ ∪ m₂ → k ∉ m₂ → k ∈ m₁