mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.Galois.Basic
/-- Let $E / F$ be a finite extension of fields. If $E$ is Galois over $F$, then
$|\text{Aut}(E/F)| = [E : F]$.  -/
IsGalois.card_aut_eq_finrank : ∀ (F : Type u_1) [inst : Field F] (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E] [FiniteDimensional F E]
  [IsGalois F E], Nat.card Gal(E/F) = Module.finrank F E
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.isSeparatedFor_iff_generate : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X},
  CategoryTheory.Presieve.IsSeparatedFor P R ↔
    CategoryTheory.Presieve.IsSeparatedFor P (CategoryTheory.Sieve.generate R).arrows
-- Mathlib.Data.Fintype.Sets
Set.toFinset_range : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype β] (f : β → α)
  [inst_2 : Fintype ↑(Set.range f)], (Set.range f).toFinset = Finset.image f Finset.univ
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
/-- `Tor` can be computed using a projective resolution.  -/
Rep.torIso : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) →
        {B : Rep.{u, u, u} k G} →
          (P : CategoryTheory.ProjectiveResolution B) →
            (n : ℕ) →
              ((Rep.Tor k G n).obj A).obj B ≅
                HomologicalComplex.homology (HomologicalComplex.coinvariantsTensorObj A P.complex) n
-- Mathlib.Algebra.Category.BoolRing
BoolRing.of.inj : ∀ {carrier : Type u} {booleanRing : BooleanRing carrier} {carrier_1 : Type u} {booleanRing_1 : BooleanRing carrier_1},
  { carrier := carrier, booleanRing := booleanRing } = { carrier := carrier_1, booleanRing := booleanRing_1 } →
    carrier = carrier_1 ∧ booleanRing ≍ booleanRing_1
-- Init.Data.BitVec.Lemmas
BitVec.toFin_sshiftRight : ∀ {w : ℕ} {x : BitVec w} {n : ℕ},
  (x.sshiftRight n).toFin =
    if x.msb = true then Fin.ofNat (2 ^ w) (2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> n)
    else Fin.ofNat (2 ^ w) (x.toNat >>> n)
-- Init.Data.SInt.Lemmas
Int16.toInt_div : ∀ (a b : Int16), (a / b).toInt = (a.toInt.tdiv b.toInt).bmod (2 ^ 16)
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.IsPresentation.bijective : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] {solution : relations.Solution M},
  solution.IsPresentation → Function.Bijective ⇑solution.fromQuotient
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Module.FaithfullyFlat.lTensor_nontrivial : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [Module.FaithfullyFlat R M] (N : Type u_1) [inst_4 : AddCommGroup N] [inst_5 : Module R N] [Nontrivial N],
  Nontrivial (TensorProduct R M N)
-- Mathlib.Probability.Distributions.Binomial
ProbabilityTheory.binomial_real_self : ∀ (n : ℕ) (p : ↑unitInterval), (ProbabilityTheory.binomial n p).real {n} = ↑p ^ n
-- Mathlib.Analysis.InnerProductSpace.Basic
DFinsupp.inner_sum : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} [inst_3 : DecidableEq ι] {α : ι → Type u_5} [inst_4 : (i : ι) → AddZeroClass (α i)]
  [inst_5 : (i : ι) → (x : α i) → Decidable (x ≠ 0)] (f : (i : ι) → α i → E) (l : Π₀ (i : ι), α i) (x : E),
  inner 𝕜 x (l.sum f) = l.sum fun i a => inner 𝕜 x (f i a)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- Subsemiring closure of a set is monotone in its argument: if `s ⊆ t`,
then `closure s ≤ closure t`.  -/
Subsemiring.closure_mono : ∀ {R : Type u} [inst : NonAssocSemiring R] ⦃s t : Set R⦄, s ⊆ t → Subsemiring.closure s ≤ Subsemiring.closure t
-- Mathlib.Util.Export
Lean.Export.Entry.level.injEq : ∀ (n n_1 : Lean.Level), (Lean.Export.Entry.level n = Lean.Export.Entry.level n_1) = (n = n_1)
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.toPrenex.eq_4 : ∀ {L : FirstOrder.Language} {α : Type u'} (x : ℕ) (f₁ f₂ : L.BoundedFormula α x),
  (f₁.imp f₂).toPrenex = f₁.toPrenex.toPrenexImp f₂.toPrenex
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.revAt_add : ∀ {N O n o : ℕ}, n ≤ N → o ≤ O → (Polynomial.revAt (N + O)) (n + o) = (Polynomial.revAt N) n + (Polynomial.revAt O) o
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.instDecidableEqHom : {n m : SimplexCategory} → DecidableEq (n ⟶ m)
-- Mathlib.LinearAlgebra.Projection
/-- Idempotent operators are equal iff their range and kernels are.  -/
LinearMap.IsIdempotentElem.ext_iff : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : E →ₗ[R] E},
  IsIdempotentElem p → IsIdempotentElem q → (p = q ↔ p.range = q.range ∧ p.ker = q.ker)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_insert_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited β] {k : α} {v : β}, (m.insert k v)[k]! = v
-- Init.Core
/-- Monadic iteration in `do`-blocks, using the `for x in xs` notation.

The parameter `m` is the monad of the `do`-block in which iteration is performed, `ρ` is the type of
the collection being iterated over, and `α` is the type of elements.
 -/
ForIn : (Type u₁ → Type u₂) → Type u → outParam (Type v) → Type (max (max (max u (u₁ + 1)) u₂) v)
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instInhabitedLambdaTheoremType : Inhabited Mathlib.Meta.FunProp.LambdaTheoremType
-- Mathlib.Topology.UniformSpace.Basic
map_uniformity_set_coe : ∀ {α : Type ua} {s : Set α} [inst : UniformSpace α],
  Filter.map (Prod.map Subtype.val Subtype.val) (uniformity ↑s) = uniformity α ⊓ Filter.principal (s ×ˢ s)
-- Init.System.IO
/-- Blocks until the child process has exited and returns its exit code.
 -/
IO.Process.Child.wait : {cfg : IO.Process.StdioConfig} → IO.Process.Child cfg → IO UInt32
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.excenter_eq_excenter_iff : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n}
  {signs₁ signs₂ : Finset (Fin (n + 1))},
  s.ExcenterExists signs₁ →
    s.ExcenterExists signs₂ → (s.excenter signs₁ = s.excenter signs₂ ↔ signs₁ = signs₂ ∨ signs₁ = signs₂ᶜ)
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.nonneg_subConst_self : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] {A : Finset G}, A.Nonempty → 1 ≤ A.subConst A
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mapIso_inverse_map_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S S' : D} {T : CategoryTheory.Functor C D} (i : S ≅ S')
  {X Y : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S') T} (f : X ⟶ Y),
  ((CategoryTheory.StructuredArrow.mapIso i).inverse.map f).right = f.right
-- Mathlib.Data.ZMod.Basic
ZMod.ker_intCastAddHom : ∀ (n : ℕ), (Int.castAddHom (ZMod n)).ker = AddSubgroup.zmultiples ↑n
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
nhdsWithin_Iic_isMeasurablyGenerated : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : Preorder α]
  {a b : α} [ClosedIicTopology α], (nhdsWithin a (Set.Iic b)).IsMeasurablyGenerated
-- Aesop.RuleSet.Member
Aesop.BaseRuleSetMember.safeRule.injEq : ∀ (r r_1 : Aesop.SafeRule), (Aesop.BaseRuleSetMember.safeRule r = Aesop.BaseRuleSetMember.safeRule r_1) = (r = r_1)
-- Mathlib.Order.Directed
Antitone.directed_ge : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [IsDirectedOrder α] [inst_2 : Preorder β] {f : α → β},
  Antitone f → Directed (fun x1 x2 => x2 ≤ x1) f
-- Mathlib.Order.Category.FinBoolAlg
/-- The equivalence between `FinBoolAlg` and itself induced by `OrderDual` both ways.  -/
FinBoolAlg.dualEquiv : FinBoolAlg ≌ FinBoolAlg
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.PendingSolverPropagations.mk.inj : ∀ {data data_1 : Lean.Meta.Grind.PendingSolverPropagationsData✝}, { data := data } = { data := data_1 } → data = data_1
-- Batteries.Data.Fin.Fold
Fin.dfoldrM_loop_zero : ∀ {m : Type u_1 → Type u_2} {n : ℕ} {α : Fin (n + 1) → Type u_1} {h : 0 < n + 1} [inst : Monad m]
  (f : (i : Fin n) → α i.succ → m (α i.castSucc)) (x : α ⟨0, h⟩), Fin.dfoldrM.loop n α f 0 h x = pure x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_of_contains_filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : (a : α) → β a → Bool} {k : α},
  m.WF → (Std.DHashMap.Raw.filter f m).contains k = true → m.contains k = true
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw.toArray_eq_toArray_toListModel : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β},
  m.toArray = (Std.DHashMap.Internal.toListModel m.buckets).toArray
-- Mathlib.Algebra.Order.Group.Basic
zpow_right_strictMono : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] {a : α},
  1 < a → StrictMono fun n => a ^ n
-- Mathlib.Algebra.Module.LinearMap.Rat
AddMonoidHom.coe_toRatLinearMap : ∀ {M : Type u_1} {M₂ : Type u_2} [inst : AddCommGroup M] [inst_1 : Module ℚ M] [inst_2 : AddCommGroup M₂]
  [inst_3 : Module ℚ M₂] (f : M →+ M₂), ⇑f.toRatLinearMap = ⇑f
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
nnnorm_cfc_le : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedAlgebra 𝕜 A] [inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p] {f : 𝕜 → 𝕜}
  {a : A} (c : NNReal), (∀ x ∈ spectrum 𝕜 a, ‖f x‖₊ ≤ c) → ‖cfc f a‖₊ ≤ c
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
/-- The largest balanced subset of `s`.  -/
balancedCore : (𝕜 : Type u_1) → {E : Type u_2} → [SeminormedRing 𝕜] → [SMul 𝕜 E] → Set E → Set E
-- Mathlib.Topology.Algebra.Group.Basic
Prod.continuousInv : ∀ {G : Type w} {H : Type x} [inst : TopologicalSpace G] [inst_1 : Inv G] [ContinuousInv G] [inst_3 : TopologicalSpace H]
  [inst_4 : Inv H] [ContinuousInv H], ContinuousInv (G × H)
-- Init.WFExtrinsicFix
/-- The function implemented as the loop `opaqueFix R F a = F a (fun a _ => opaqueFix R F a)`.
`opaqueFix R F` is the fixpoint of the functional `F`, as long as the loop is
well-founded.

The loop might run forever depending on `F`. It is opaque, i.e., it is impossible to prove
nontrivial properties about it.
 -/
_private.Init.WFExtrinsicFix.0.WellFounded.opaqueFix : {α : Sort u_1} →
  {C : α → Sort u_2} →
    [∀ (a : α), Nonempty (C a)] → (R : α → α → Prop) → ((a : α) → ((a' : α) → R a' a → C a') → C a) → (a : α) → C a
-- Mathlib.Data.Prod.Basic
Prod.map_apply' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → γ) (g : β → δ) (p : α × β),
  Prod.map f g p = (f p.1, g p.2)
-- Mathlib.Analysis.Complex.Norm
Complex.norm_natCast : ∀ (n : ℕ), ‖↑n‖ = ↑n
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso_hom_comp_homologyIso_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology] (h : S.LeftHomologyData) {Z : C} (h_1 : S.homology ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.leftHomologyIso.hom (CategoryTheory.CategoryStruct.comp h.homologyIso.inv h_1) =
    CategoryTheory.CategoryStruct.comp S.leftHomologyIso.hom h_1
-- Init.Data.String.Lemmas.Basic
String.Pos.byte_toSlice : ∀ {s : String} {p : s.Pos} {h : p.toSlice ≠ s.toSlice.endPos}, p.toSlice.byte h = p.byte ⋯
-- Mathlib.Topology.Connected.TotallyDisconnected
Continuous.connectedComponentsMap_surjective : ∀ {α : Type u} [inst : TopologicalSpace α] {β : Type u_3} [inst_1 : TopologicalSpace β] {f : α → β} (hf : Continuous f),
  Function.Surjective f → Function.Surjective hf.connectedComponentsMap
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Under.homMk_hom : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T}
  [inst_1 : Q.IsMultiplicative] {A B : P.Under Q X} (f : A.right ⟶ B.right)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp A.hom f = B.hom) CategoryTheory.MorphismProperty.Under.homMk._auto_1)
  (hf : autoParam (Q f) CategoryTheory.MorphismProperty.Under.homMk._auto_3),
  CategoryTheory.MorphismProperty.Comma.Hom.hom (CategoryTheory.MorphismProperty.Under.homMk f w hf) =
    CategoryTheory.Under.homMk f w
-- Mathlib.Algebra.Group.Units.Equiv
Equiv.subLeft_apply : ∀ {G : Type u_5} [inst : AddGroup G] (a b : G), (Equiv.subLeft a) b = a - b
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.prependMap.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2}
  (motive : Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Zipper α β → Sort u_3) (size : ℕ) (k : α) (v : β k)
  (l r : Std.DTreeMap.Internal.Impl α β) (it : Std.DTreeMap.Internal.Zipper α β)
  (h_1 : (it : Std.DTreeMap.Internal.Zipper α β) → motive Std.DTreeMap.Internal.Impl.leaf it)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (it : Std.DTreeMap.Internal.Zipper α β) → motive (Std.DTreeMap.Internal.Impl.inner size k v l r) it),
  (match Std.DTreeMap.Internal.Impl.inner size k v l r, it with
    | Std.DTreeMap.Internal.Impl.leaf, it => h_1 it
    | Std.DTreeMap.Internal.Impl.inner size k v l r, it => h_2 size k v l r it) =
    h_2 size k v l r it
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Bialgebra.TensorProduct.lid_toAlgEquiv : ∀ {R : Type u_1} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring B] [inst_2 : Bialgebra R B],
  (Bialgebra.TensorProduct.lid R B).toAlgEquiv = Algebra.TensorProduct.lid R B
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.comap_const : ∀ {R : Type u} [inst : CommRing R] {S : Type u} [inst_1 : CommRing S] (f : R →+* S)
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
  (V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top S))
  (hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier) (a b : R) (hb : ∀ x ∈ U, b ∈ x.asIdeal.primeCompl),
  (AlgebraicGeometry.StructureSheaf.comap f U V hUV) (AlgebraicGeometry.StructureSheaf.const a b U hb) =
    AlgebraicGeometry.StructureSheaf.const (f a) (f b) V ⋯
-- Mathlib.Analysis.Calculus.TangentCone.DimOne
/-- The tangent cone at a non-isolated point in dimension 1 is the whole space.  -/
tangentConeAt_eq_univ : ∀ {𝕜 : Type u_1} [inst : NormedDivisionRing 𝕜] {s : Set 𝕜} {x : 𝕜},
  AccPt x (Filter.principal s) → tangentConeAt 𝕜 s x = Set.univ
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instZeroOfAddOpposite.eq_1 : ∀ {M : Type u_1} [inst : Zero Mᵃᵒᵖ], DomAddAct.instZeroOfAddOpposite = inst
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.compl_iInf : ∀ {α : Type u_1} {ι : Sort u_4} [inst : LE α] (f : ι → LowerSet α), (⨅ i, f i).compl = ⨅ i, (f i).compl
-- Mathlib.RingTheory.TwoSidedIdeal.Lattice
TwoSidedIdeal.mem_sup_right : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] {I J : TwoSidedIdeal R} {x : R}, x ∈ J → x ∈ I ⊔ J
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
CliffordAlgebra.ι_mul_ι_mul_of_isOrtho : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (x : CliffordAlgebra Q) {a b : M},
  QuadraticMap.IsOrtho Q a b →
    (CliffordAlgebra.ι Q) a * ((CliffordAlgebra.ι Q) b * x) = -((CliffordAlgebra.ι Q) b * ((CliffordAlgebra.ι Q) a * x))
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.bot_boxes : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι}, ⊥.boxes = ∅
-- Aesop.Tree.AddRapp
Aesop.AddRapp.consumedForwardRuleMatches : Aesop.AddRapp → Array Aesop.ForwardRuleMatch
-- Mathlib.Algebra.Group.Subgroup.Finite
AddSubgroup.card_le_of_le : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G} [Finite ↥K], H ≤ K → Nat.card ↥H ≤ Nat.card ↥K
-- Mathlib.Data.DFinsupp.Order
DFinsupp.support_inf_union_support_sup : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : (i : ι) → Lattice (α i)]
  (f g : Π₀ (i : ι), α i) [inst_2 : DecidableEq ι] [inst_3 : (i : ι) → (x : α i) → Decidable (x ≠ 0)],
  (f ⊓ g).support ∪ (f ⊔ g).support = f.support ∪ g.support
-- Mathlib.Algebra.Module.ZMod
/-- `AddMonoidHom.toZModLinearMap` as an equivalence.  -/
AddMonoidHom.toZModLinearMapEquiv : (n : ℕ) →
  {M : Type u_1} →
    {M₁ : Type u_2} →
      [inst : AddCommGroup M] →
        [inst_1 : AddCommGroup M₁] →
          [inst_2 : Module (ZMod n) M] → [inst_3 : Module (ZMod n) M₁] → (M →+ M₁) ≃+ (M →ₗ[ZMod n] M₁)
-- Mathlib.Order.Filter.Map
Filter.map_biInf_eq : ∀ {α : Type u_1} {β : Type u_2} {ι : Type w} {f : ι → Filter α} {m : α → β} {p : ι → Prop},
  DirectedOn (f ⁻¹'o fun x1 x2 => x1 ≥ x2) {x | p x} →
    (∃ i, p i) → Filter.map m (⨅ i, ⨅ (_ : p i), f i) = ⨅ i, ⨅ (_ : p i), Filter.map m (f i)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
nullMeasurableSet_Ioi : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : LinearOrder α]
  {a : α} {μ : MeasureTheory.Measure α} [ClosedIicTopology α], MeasureTheory.NullMeasurableSet (Set.Ioi a) μ
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.mk_α_inv : ∀ {C : Type u} {X Y Z : CategoryTheory.FreeMonoidalCategory C},
  ⟦CategoryTheory.FreeMonoidalCategory.Hom.α_inv X Y Z⟧ = (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.mk.sizeOf_spec : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace Z] {proj : Z → B} [inst_3 : SizeOf B] [inst_4 : SizeOf F] [inst_5 : SizeOf Z]
  (toOpenPartialHomeomorph : OpenPartialHomeomorph Z (B × F)) (baseSet : Set B) (open_baseSet : IsOpen baseSet)
  (source_eq : toOpenPartialHomeomorph.source = proj ⁻¹' baseSet)
  (target_eq : toOpenPartialHomeomorph.target = baseSet ×ˢ Set.univ)
  (proj_toFun : ∀ p ∈ toOpenPartialHomeomorph.source, (↑toOpenPartialHomeomorph p).1 = proj p),
  sizeOf
      { toOpenPartialHomeomorph := toOpenPartialHomeomorph, baseSet := baseSet, open_baseSet := open_baseSet,
        source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun } =
    1 + sizeOf toOpenPartialHomeomorph + sizeOf open_baseSet + sizeOf source_eq + sizeOf target_eq
-- Init.Data.SInt.Bitwise
Int16.toInt64_and : ∀ (a b : Int16), (a &&& b).toInt64 = a.toInt64 &&& b.toInt64
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.mkInjectiveEqTheoremValue : Lean.ConstructorVal → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Combinatorics.SimpleGraph.UniversalVerts
SimpleGraph.isClique_universalVerts : ∀ {V : Type u_1} (G : SimpleGraph V), G.IsClique G.universalVerts
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RcoSliceData.range : {α : Type u} → [inst : Ord α] → Std.DTreeMap.Internal.Unit.RcoSliceData α → Std.Rco α
-- Mathlib.AlgebraicGeometry.Morphisms.Proper
AlgebraicGeometry.IsProper.mk : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [toIsSeparated : AlgebraicGeometry.IsSeparated f]
  [toUniversallyClosed : AlgebraicGeometry.UniversallyClosed f]
  [toLocallyOfFiniteType : AlgebraicGeometry.LocallyOfFiniteType f], AlgebraicGeometry.IsProper f
-- Lean.Elab.Quotation.Precheck
Lean.Elab.Term.Quotation.withNewLocal : {α : Type} → Lean.Name → Lean.Elab.Term.Quotation.PrecheckM α → Lean.Elab.Term.Quotation.PrecheckM α
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.instIsDenseSubsiteOpensCarrierCarrierCommRingCatGrothendieckTopologyGrothendieckTopologyToOpensFunctor : ∀ {X : AlgebraicGeometry.Scheme},
  CategoryTheory.Functor.IsDenseSubsite (AlgebraicGeometry.Scheme.AffineZariskiSite.grothendieckTopology X)
    (Opens.grothendieckTopology ↥X) (AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor X)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.zero_point : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} [inst_1 : Nontrivial R],
  WeierstrassCurve.Jacobian.Point.point 0 = ⟦![1, 1, 0]⟧
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
ContinuousLinearEquiv.uniformConvergenceCLMCongrSL_apply : ∀ {𝕜 : Type u_6} {𝕜₂ : Type u_7} {𝕜₃ : Type u_8} {𝕜₄ : Type u_9} {E : Type u_10} {F : Type u_11} {G : Type u_12}
  {H : Type u_13} [inst : AddCommGroup E] [inst_1 : AddCommGroup F] [inst_2 : AddCommGroup G] [inst_3 : AddCommGroup H]
  [inst_4 : NormedField 𝕜] [inst_5 : NormedField 𝕜₂] [inst_6 : NormedField 𝕜₃] [inst_7 : NormedField 𝕜₄]
  [inst_8 : Module 𝕜 E] [inst_9 : Module 𝕜₂ F] [inst_10 : Module 𝕜₃ G] [inst_11 : Module 𝕜₄ H]
  [inst_12 : TopologicalSpace E] [inst_13 : TopologicalSpace F] [inst_14 : TopologicalSpace G]
  [inst_15 : TopologicalSpace H] [inst_16 : IsTopologicalAddGroup G] [inst_17 : IsTopologicalAddGroup H]
  [inst_18 : ContinuousConstSMul 𝕜₃ G] [inst_19 : ContinuousConstSMul 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜}
  {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄}
  [inst_20 : RingHomInvPair σ₁₂ σ₂₁] [inst_21 : RingHomInvPair σ₂₁ σ₁₂] [inst_22 : RingHomInvPair σ₃₄ σ₄₃]
  [inst_23 : RingHomInvPair σ₄₃ σ₃₄] [inst_24 : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄] [inst_25 : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃]
  [inst_26 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_27 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄]
  [inst_28 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [inst_29 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] (e₁₂ : E ≃SL[σ₁₂] F)
  (e₄₃ : H ≃SL[σ₄₃] G) (𝔖 : Set (Set E)) (𝔗 : Set (Set F)) (h : ⋯), ⋯
-- Mathlib.GroupTheory.Goursat
/-- **Goursat's lemma** for an arbitrary subgroup.

If `I` is a subgroup of `G × H`, then there exist subgroups `G' ≤ G`, `H' ≤ H` and normal subgroups
`M ≤ G'` and `N ≤ H'` such that `M × N ≤ I` and the image of `I` in `G' ⧸ M × H' ⧸ N` is the graph
of an isomorphism `G ⧸ G' ≃ H ⧸ H'`.  -/
AddSubgroup.goursat : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] {I : AddSubgroup (G × H)},
  ∃ G' H' M N,
    ∃ (x : M.Normal) (x_1 : N.Normal),
      ∃ e,
        I =
          AddSubgroup.map (G'.subtype.prodMap H'.subtype)
            (AddSubgroup.comap ((QuotientAddGroup.mk' M).prodMap (QuotientAddGroup.mk' N)) e.toAddMonoidHom.graph)
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- TODO: generalize `Submodule.map₂` to semilinear maps, so that we can state
`U ⟂ V ↔ Submodule.map₂ (innerₛₗ 𝕜) U V ≤ ⊥`.  -/
Submodule.isOrtho_bot_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {V : Submodule 𝕜 E}, ⊥ ⟂ V
-- Mathlib.MeasureTheory.Function.LpSeminorm.Defs
/-- The property that `f : α → E` is a.e. strongly measurable and `(∫ ‖f a‖ ^ p ∂μ) ^ (1/p)`
is finite if `p < ∞`, or `essSup ‖f‖ < ∞` if `p = ∞`.  -/
MeasureTheory.MemLp : {α : Type u_1} →
  {ε : Type u_2} →
    {m0 : MeasurableSpace α} →
      [ENorm ε] →
        [TopologicalSpace ε] →
          (α → ε) → ENNReal → autoParam (MeasureTheory.Measure α) MeasureTheory.MemLp._auto_1 → Prop
-- Mathlib.Order.WithBot
WithTop.ofDual_symm : ∀ {α : Type u_1}, WithTop.ofDual.symm = WithBot.toDual
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.mem_iSup_prop : ∀ {G : Type u_1} [inst : Group G] {p : Prop} {K : p → Subgroup G} {x : G},
  x ∈ ⨆ (h : p), K h ↔ x = 1 ∨ ∃ (h : p), x ∈ K h
-- Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Matrix.GeneralLinearGroup.fin_two_smul_prod : ∀ {R : Type u_3} [inst : CommRing R] (g : GL (Fin 2) R) (v : R × R),
  g • v = (↑g 0 0 * v.1 + ↑g 0 1 * v.2, ↑g 1 0 * v.1 + ↑g 1 1 * v.2)
-- Batteries.Data.List.Matcher
/-- Returns all the start and end positions of all infix sublists of of `l` that match `pattern`.
The sublists may be overlapping.
 -/
List.findAllInfix : {α : Type u_1} → [BEq α] → List α → List α → Array (ℕ × ℕ)