mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Decode
Char.utf8Size.eq_def : ∀ (c : Char),
  c.utf8Size =
    have v := c.val;
    if v ≤ UInt32.ofNatLT 127 Char.utf8Size._proof_1 then 1
    else
      if v ≤ UInt32.ofNatLT 2047 Char.utf8Size._proof_2 then 2
      else if v ≤ UInt32.ofNatLT 65535 Char.utf8Size._proof_3 then 3 else 4
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.comap_comp : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] {F : Type u_3} [inst_2 : Field F]
  (w : NumberField.InfinitePlace K) (f : F →+* K) (g : k →+* F), w.comap (f.comp g) = (w.comap f).comap g
-- Qq.Macro
/-- New free variables in the new context that were newly introduced for irreducible expressions.  -/
Qq.Impl.UnquoteState.abstractedFVars : Qq.Impl.UnquoteState → Array Lean.FVarId
-- Mathlib.CategoryTheory.GradedObject.Braiding
CategoryTheory.GradedObject.braidedCategory : {I : Type u_1} →
  [inst : AddCommMonoid I] →
    {C : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_1, u_2} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : ∀ (X₁ X₂ : CategoryTheory.GradedObject I C), X₁.HasTensor X₂] →
            [inst_4 : ∀ (X₁ X₂ X₃ : CategoryTheory.GradedObject I C), X₁.HasGoodTensor₁₂Tensor X₂ X₃] →
              [inst_5 : ∀ (X₁ X₂ X₃ : CategoryTheory.GradedObject I C), X₁.HasGoodTensorTensor₂₃ X₂ X₃] →
                [inst_6 : DecidableEq I] →
                  [inst_7 : CategoryTheory.Limits.HasInitial C] →
                    [inst_8 :
                        ∀ (X₁ : C),
                          CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
                            ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)] →
                      [inst_9 :
                          ∀ (X₂ : C),
                            CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
                              ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)] →
                        [inst_10 : ∀ (X₁ X₂ X₃ X₄ : CategoryTheory.GradedObject I C), X₁.HasTensor₄ObjExt X₂ X₃ X₄] →
                          [CategoryTheory.BraidedCategory C] →
                            CategoryTheory.BraidedCategory (CategoryTheory.GradedObject I C)
-- Mathlib.Order.ModularLattice
/-- A disjoint element can be enlarged to a complementary element.  -/
Disjoint.exists_isCompl : ∀ {α : Type u_1} [inst : Lattice α] [IsModularLattice α] [inst_2 : BoundedOrder α] [ComplementedLattice α] {a b : α},
  Disjoint a b → ∃ a', a ≤ a' ∧ IsCompl a' b
-- Mathlib.Topology.Algebra.Support
HasCompactSupport.comp₂_left : ∀ {α : Type u_2} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [inst : TopologicalSpace α] [inst_1 : Zero β]
  [inst_2 : Zero γ] [inst_3 : Zero δ] {f : α → β} {f₂ : α → γ} {m : β → γ → δ},
  HasCompactSupport f → HasCompactSupport f₂ → m 0 0 = 0 → HasCompactSupport fun x => m (f x) (f₂ x)
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.ClassifyResult.nonCommRing : ℕ → Lean.Meta.Sym.Arith.ClassifyResult
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.kernel_eq_kernel : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c)
  [inst_2 : CategoryTheory.Limits.HasKernels V] {i j j' : ι},
  c.Rel i j →
    c.Rel i j' → CategoryTheory.Limits.kernelSubobject (C.d i j) = CategoryTheory.Limits.kernelSubobject (C.d i j')
-- Lean.Meta.Tactic.Grind.Inv
_private.Lean.Meta.Tactic.Grind.Inv.0.Lean.Meta.Grind.checkPtrEqImpliesStructEq : Lean.Meta.Grind.GoalM Unit
-- Std.Data.TreeMap.Raw.Basic
/-- Erases multiple mappings from the tree map by iterating over the given collection and calling
`erase`.
 -/
Std.TreeMap.Raw.eraseMany : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} → {ρ : Type u_1} → [ForIn Id ρ α] → Std.TreeMap.Raw α β cmp → ρ → Std.TreeMap.Raw α β cmp
-- Mathlib.Data.List.Defs
/-- Length of the list obtained by `mapAccumr`.  -/
List.length_mapAccumr : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → γ → γ × β) (x : List α) (s : γ),
  (List.mapAccumr f x s).2.length = x.length
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.comm : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp}, t₁.Equiv t₂ ↔ t₂.Equiv t₁
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.instOrderBot : {α : Type u_1} → {β : Type u_2} → OrderBot (Graph α β)
-- Mathlib.Topology.Algebra.Module.Basic
Submodule.topologicalClosure_mono : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : ContinuousConstSMul R M] [inst_5 : ContinuousAdd M] {s t : Submodule R M},
  s ≤ t → s.topologicalClosure ≤ t.topologicalClosure
-- Init.Data.SInt.Lemmas
Int32.eq_iff_toBitVec_eq : ∀ {a b : Int32}, a = b ↔ a.toBitVec = b.toBitVec
-- Mathlib.RingTheory.HopkinsLevitzki
IsNoetherianRing.isArtinianRing_of_krullDimLE_zero : ∀ {R : Type u_3} [inst : CommRing R] [IsNoetherianRing R] [Ring.KrullDimLE 0 R], IsArtinianRing R
-- Mathlib.Topology.Baire.BaireMeasurable
closure_residualEq : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α}, IsLocallyClosed s → closure s =ᶠ[residual α] s
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.getEntry!.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) [inst_1 : Inhabited ((a : α) × β a)] (k : α) (v : β k)
  (l : List ((a : α) × β a)),
  Std.Internal.List.getEntry! a (⟨k, v⟩ :: l) = bif k == a then ⟨k, v⟩ else Std.Internal.List.getEntry! a l
-- Mathlib.Data.Finset.Card
/-- Given an injective map `f` defined on a finite set `s` to another finite set `t`, if `t` is no
larger than `s`, then `f` is surjective to `t` when restricted to `s`.
See `Finset.surjOn_of_injOn_of_card_le` for the version where `f` is a non-dependent function.
 -/
Finset.surj_on_of_inj_on_of_card_le : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (f : (a : α) → a ∈ s → β),
  (∀ (a : α) (ha : a ∈ s), f a ha ∈ t) →
    (∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂) →
      t.card ≤ s.card → ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), b = f a ha
-- Mathlib.Data.Fin.Basic
/-- `Fin.le_or_gt` is an alias of `Fin.le_or_lt`.
It is preferred since it follows the mathlib naming convention.  -/
Fin.le_or_gt : ∀ {n : ℕ} (a b : Fin n), a ≤ b ∨ b < a
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.invRev_bijective : ∀ {α : Type u}, Function.Bijective FreeGroup.invRev
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.natTrailingDegree_eq_of_trailingDegree_eq_some : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, p.trailingDegree = ↑n → p.natTrailingDegree = n
-- Lean.Meta.Tactic.Grind.Split
/-- Performs a case-split using `c`.
Remark: `numCases` and `isRec` are computed using `checkSplitStatus`.
 -/
Lean.Meta.Grind.Action.splitCore : Lean.Meta.Grind.SplitInfo →
  ℕ → Bool → Bool → Bool → optParam (Option (List Lean.Meta.Grind.SplitInfo)) none → Lean.Meta.Grind.Action
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.K'.rev.sizeOf_spec : sizeOf Turing.PartrecToTM2.K'.rev = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.imageMonoIsoSource_inv_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f] {Z : C}
  (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageMonoIsoSource f).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.ne_zero' : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i : ι) [NeZero 2],
  P.coroot i ≠ 0
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Arg.updateType! : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Arg pu → Lean.Expr → Lean.Compiler.LCNF.Arg pu
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- **Alias** of `zero_apply`. -/
MeasureTheory.VectorMeasure.zero_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Zero β}
  {inst_2 : Zero F} [self : IsZeroApply F α β] (x : α), 0 x = 0
-- Mathlib.MeasureTheory.Measure.ContinuousPreimage
/-- **Alias** of `MeasureTheory.isClosed_setOfPred_preimage_ae_eq`.

---

Let `f : Z → C(X, Y)` be a continuous (in the compact open topology) family
of continuous measure-preserving maps.
Let `t : Set Y` be a null measurable set of finite measure.
Then for any `s`, the set of parameters `z`
such that the preimage of `t` under `f_z` is a.e. equal to `s`
is a closed set.

In particular, if `X = Y` and `s = t`,
then we see that the a.e. stabilizer of a set is a closed set.  -/
MeasureTheory.isClosed_setOf_preimage_ae_eq : ∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [BorelSpace X]
  [R1Space X] [inst_4 : TopologicalSpace Y] [inst_5 : MeasurableSpace Y] [BorelSpace Y] [R1Space Y]
  [inst_8 : TopologicalSpace Z] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [μ.InnerRegularCompactLTTop]
  [MeasureTheory.IsLocallyFiniteMeasure ν] {f : Z → C(X, Y)},
  Continuous f →
    (∀ (z : Z), MeasureTheory.MeasurePreserving (⇑(f z)) μ ν) →
      ∀ (s : Set X) {t : Set Y}, MeasureTheory.NullMeasurableSet t ν → ν t ≠ ⊤ → IsClosed {z | ⇑(f z) ⁻¹' t =ᵐ[μ] s}
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.instMembership.eq_1 : ∀ {α : Type u_1}, FreeMonoid.instMembership = { mem := FreeMonoid.mem }
-- Mathlib.Order.Filter.AtTopBot.BigOperators
/-- Let `f` and `g` be two maps to the same commutative monoid. This lemma gives a sufficient
condition for comparison of the filter `atTop.map (fun s ↦ ∏ b ∈ s, f b)` with
`atTop.map (fun s ↦ ∏ b ∈ s, g b)`. This is useful to compare the set of limit points of
`Π b in s, f b` as `s → atTop` with the similar set for `g`.  -/
Filter.map_atTop_finsetProd_le_of_prod_eq : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : CommMonoid M] {f : α → M} {g : β → M},
  (∀ (u : Finset β), ∃ v, ∀ (v' : Finset α), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b) →
    Filter.map (fun s => ∏ b ∈ s, f b) Filter.atTop ≤ Filter.map (fun s => ∏ x ∈ s, g x) Filter.atTop
-- Mathlib.Probability.Process.LocalProperty
_private.Mathlib.Probability.Process.LocalProperty.0.ProbabilityTheory.isPreLocalizingSequence_of_isLocalizingSequence_aux' : ∀ {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [inst : ConditionallyCompleteLinearOrderBot ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι]
  {𝓕 : MeasureTheory.Filtration ι mΩ} [SecondCountableTopology ι] [MeasureTheory.IsFiniteMeasure P]
  {τ : ℕ → Ω → WithTop ι} {σ : ℕ → ℕ → Ω → WithTop ι},
  ProbabilityTheory.IsLocalizingSequence 𝓕 τ P →
    (∀ (n : ℕ), ProbabilityTheory.IsLocalizingSequence 𝓕 (σ n) P) →
      ∃ T,
        Filter.Tendsto T Filter.atTop Filter.atTop ∧ ∀ (n : ℕ), ∃ k, P {ω | σ n k ω < min (τ n ω) ↑(T n)} ≤ (1 / 2) ^ n
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.rel_π₂ : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} (c₁ : ComplexShape I₁) {c₂ : ComplexShape I₂}
  (c₁₂ : ComplexShape I₁₂) [inst : TotalComplexShape c₁ c₂ c₁₂] (i₁ : I₁) {i₂ i₂' : I₂},
  c₂.Rel i₂ i₂' → c₁₂.Rel (c₁.π c₂ c₁₂ (i₁, i₂)) (c₁.π c₂ c₁₂ (i₁, i₂'))
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get!_eq_getElem! : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {a : α}, m.get! a = m[a]!
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.endofunctorMonoidalCategory_tensorUnit_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor C C)).map f = f
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofCommaSndEquivalence_counitIso : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T)
  (G : CategoryTheory.Functor D T) (c : C),
  (CategoryTheory.StructuredArrow.ofCommaSndEquivalence F G c).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun x =>
        CategoryTheory.Iso.refl
          (((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse F G c).comp
                (CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor F G c)).obj
            x))
      ⋯
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
ProfiniteGrp.ProfiniteCompletion.preimage.eq_1 : ∀ {G : GrpCat} {P : ProfiniteGrp.{u}} (f : G ⟶ GrpCat.of ↑P.toProfinite.toTop)
  (H : OpenNormalSubgroup ↑P.toProfinite.toTop),
  ProfiniteGrp.ProfiniteCompletion.preimage f H =
    FiniteIndexNormalSubgroup.comap (GrpCat.Hom.hom f) H.toFiniteIndexNormalSubgroup
-- Mathlib.RingTheory.Ideal.Defs
Ideal.instIsTwoSided_1 : ∀ {α : Type u_1} [inst : CommRing α] (I : Ideal α), I.IsTwoSided
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.mul_univ_of_one_mem : ∀ {α : Type u_2} [inst : Monoid α] {s : Set α}, 1 ∈ s → s * Set.univ = Set.univ
-- Init.Data.Slice.List.Lemmas
ListSlice.size_mkSlice_roo : ∀ {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ},
  Std.Slice.size (Std.Roo.Sliceable.mkSlice xs lo<...hi) = min hi (Std.Slice.size xs) - (lo + 1)
-- Mathlib.Data.Nat.Bitwise
Nat.xor_one_of_even : ∀ {n : ℕ}, Even n → n ^^^ 1 = n + 1
-- Mathlib.Algebra.Group.ULift
ULift.one.eq_1 : ∀ {α : Type u} [inst : One α], ULift.one = { one := { down := 1 } }
-- Mathlib.Analysis.Real.Sqrt
NNReal.sqrt_pos : ∀ {x : NNReal}, 0 < NNReal.sqrt x ↔ 0 < x
-- Mathlib.RingTheory.AdicCompletion.Completeness
AdicCompletion.ofPowSMul_ofValEqZero : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {n : ℕ} {x : AdicCompletion I M} (hxn : ↑x n = 0),
  (AdicCompletion.ofPowSMul I M n) (AdicCompletion.ofValEqZero I hxn) = x
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- `MeromorphicNFOn` is invariant under translation, special case where the set is a ball.  -/
meromorphicNFOn_ball_comp_sub_const_iff_meromorphicNFOn_ball : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {c : 𝕜} {R : ℝ},
  MeromorphicNFOn (f ∘ fun x => x - c) (Metric.ball c R) ↔ MeromorphicNFOn f (Metric.ball 0 R)
-- Mathlib.Data.ENNReal.Inv
ENNReal.inv_le_inv' : ∀ {a b : ENNReal}, a ≤ b → b⁻¹ ≤ a⁻¹
-- Mathlib.LinearAlgebra.Matrix.Ideal
_private.Mathlib.LinearAlgebra.Matrix.Ideal.0.TwoSidedIdeal.jacobson_matrix_le : ∀ {R : Type u_1} [inst : Ring R] {n : Type u_2} [inst_1 : Fintype n] [inst_2 : DecidableEq n] (I : TwoSidedIdeal R),
  (TwoSidedIdeal.matrix n I).jacobson ≤ TwoSidedIdeal.matrix n I.jacobson
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
/-- Product rule for Lie brackets: given two vector fields `V` and `W` on `M` and a function
`f : M → 𝕜`, we have `[V, f • W] = (df V) • W + f • [V, W]`. Version within a set.
 -/
VectorField.mlieBracketWithin_smul_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {x : M} {V W : (x : M) → TangentSpace I x}
  [inst_6 : IsManifold I 2 M] [CompleteSpace E] {f : M → 𝕜},
  MDiffAt[s] f x →
    (MDiffAt[s] fun x => ⟨x, W x⟩) x →
      UniqueMDiffAt[s] x →
        VectorField.mlieBracketWithin I V (f • W) s x =
          (d[s] f x) (V x) • W x + f x • VectorField.mlieBracketWithin I V W s x
-- Init.Core
Char.mk.injEq : ∀ (val : UInt32) (valid : val.isValidChar) (val_1 : UInt32) (valid_1 : val_1.isValidChar),
  ({ val := val, valid := valid } = { val := val_1, valid := valid_1 }) = (val = val_1)
-- Mathlib.Combinatorics.Additive.Corner.Defs
/-- Corners are preserved under `2`-Freiman homomorphisms.  -/
IsCornerFree.of_image : ∀ {G : Type u_1} {H : Type u_2} [inst : AddCommMonoid G] [inst_1 : AddCommMonoid H] {A : Set (G × G)} {s : Set G}
  {t : Set H} {f : G → H},
  IsAddFreimanHom 2 s t f → Set.InjOn f s → A ⊆ s ×ˢ s → IsCornerFree (Prod.map f f '' A) → IsCornerFree A
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.pointReflection_fixed_iff : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] [Invertible 2] {x y : P},
  (AffineIsometryEquiv.pointReflection 𝕜 x) y = y ↔ y = x
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.card_left : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {S : Set G}, Subgroup.IsComplement S ↑H → Nat.card ↑S = H.index
-- Mathlib.Data.Set.Lattice
Set.iUnion₂_mono' : ∀ {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} {κ : ι → Sort u_8} {κ' : ι' → Sort u_11} {s : (i : ι) → κ i → Set α}
  {t : (i' : ι') → κ' i' → Set α},
  (∀ (i : ι) (j : κ i), ∃ i' j', s i j ⊆ t i' j') → ⋃ i, ⋃ j, s i j ⊆ ⋃ i', ⋃ j', t i' j'
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.opParallelPairIso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f g : X ⟶ Y),
  CategoryTheory.Limits.opParallelPairIso f g =
    Trans.trans
      (Trans.trans
        (Trans.trans (CategoryTheory.Iso.refl (CategoryTheory.Limits.parallelPair f g).op)
          (CategoryTheory.Functor.isoWhiskerRight CategoryTheory.Limits.walkingParallelPairOpEquiv.symm.unitIso
            (CategoryTheory.Limits.parallelPair f g).op))
        (CategoryTheory.Limits.walkingParallelPairOpEquiv.inverse.associator
          CategoryTheory.Limits.walkingParallelPairOpEquiv.functor (CategoryTheory.Limits.parallelPair f g).op))
      (CategoryTheory.Limits.walkingParallelPairOpEquiv.inverse.isoWhiskerLeft
        (CategoryTheory.Limits.parallelPairOpIso f g).symm)
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.den_mul_self_eq_num : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (I : FractionalIdeal S P), I.den • ↑I = Submodule.map (Algebra.linearMap R P) I.num
-- Mathlib.LinearAlgebra.Transvection.Generation
/-- If the images of `u` and `e u` in `V ⧸ e.fixedSubmodule` are linearly independent,
then `e u` does not belong to `e.fixedSubmodule ⊔ K ∙ (e u - u)`.  -/
_private.Mathlib.LinearAlgebra.Transvection.Generation.0.LinearEquiv.apply_notMem_sup_of_linearIndependent : ∀ {K : Type u_1} [inst : DivisionRing K] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module K V] {e : V ≃ₗ[K] V}
  {u : V},
  LinearIndependent K ![(↑e).fixedSubmodule.mkQ u, e.fixedReduce ((↑e).fixedSubmodule.mkQ u)] →
    e u ∉ (↑e).fixedSubmodule ⊔ K ∙ (e u - u)
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.getResultingUniverse : List Lean.InductiveType → Lean.Elab.TermElabM Lean.Level
-- Lean.CoreM
Lean.instInhabitedDeclNameGenerator : Inhabited Lean.DeclNameGenerator
-- Std.Time.Zoned.Database.TZdb
/-- Returns a `TZdb` with common fallback zoneinfo paths for Linux and macOS.
Call this once at program startup. The `TZ` and `TZDIR` environment variables
are re-read on every `getLocalZoneRules`/`getZoneRules` call, so runtime changes
to those variables are always reflected.
 -/
Std.Time.Database.TZdb.default : Std.Time.Database.TZdb
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
/-- The group homomorphism on nonsingular points induced by an algebra homomorphism `f : F →ₐ[S] K`,
where `W` is defined over a subring of a ring `S`, and `F` and `K` are field extensions of `S`.  -/
WeierstrassCurve.Affine.Point.map : {R : Type r} →
  {S : Type s} →
    {F : Type u} →
      {K : Type v} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Field F] →
              [inst_3 : Field K] →
                {W' : WeierstrassCurve.Affine R} →
                  [inst_4 : DecidableEq F] →
                    [inst_5 : DecidableEq K] →
                      [inst_6 : Algebra R S] →
                        [inst_7 : Algebra R F] →
                          [inst_8 : Algebra S F] →
                            [IsScalarTower R S F] →
                              [inst_10 : Algebra R K] →
                                [inst_11 : Algebra S K] →
                                  [IsScalarTower R S K] →
                                    (F →ₐ[S] K) → (W'.baseChange F).Point →+ (W'.baseChange K).Point
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
/-- A linear independent family of `finrank K V` vectors forms a basis.  -/
basisOfLinearIndependentOfCardEqFinrank' : {K : Type u} →
  {V : Type v} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] →
          {ι : Type u_1} →
            [inst_3 : Fintype ι] →
              [FiniteDimensional K V] →
                (b : ι → V) → LinearIndependent K b → Fintype.card ι = Module.finrank K V → Module.Basis ι K V
-- Mathlib.Algebra.ContinuedFractions.Basic
GenContFract.Pair.mk : {α : Type u_1} → α → α → GenContFract.Pair α
-- Mathlib.Analysis.Normed.Affine.MazurUlam
/-- **Mazur-Ulam Theorem**: if `f` is an isometric bijection between two normed vector spaces
over `ℝ` and `f 0 = 0`, then `f` is a linear isometry equivalence.  -/
IsometryEquiv.toRealLinearIsometryEquivOfMapZero : {E : Type u_1} →
  {F : Type u_3} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] → [inst_3 : NormedSpace ℝ F] → (f : E ≃ᵢ F) → f 0 = 0 → E ≃ₗᵢ[ℝ] F
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_compl_union_of_disjoint : ∀ {α : Type u_1} {X Y : Set α} (M : Matroid α), Disjoint X Y → M.eRk (M.E \ X ∪ Y) = M.eRk (M.E \ X)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
/-- This cannot be marked `@[ext]` as it ends up being used instead of `LinearMap.prod_ext` when
working with `R × M`.  -/
TrivSqZeroExt.linearMap_ext : ∀ {S : Type u_2} {R : Type u} {M : Type v} {N : Type u_3} [inst : Semiring S] [inst_1 : AddCommMonoid R]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module S R] [inst_5 : Module S M]
  [inst_6 : Module S N] ⦃f g : TrivSqZeroExt R M →ₗ[S] N⦄,
  (∀ (r : R), f (TrivSqZeroExt.inl r) = g (TrivSqZeroExt.inl r)) →
    (∀ (m : M), f (TrivSqZeroExt.inr m) = g (TrivSqZeroExt.inr m)) → f = g
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.max_zero_left : ∀ (a : Ordinal.{u_1}), max 0 a = a
-- Mathlib.Algebra.Group.AddChar
/-- `mulShift ψ 0` is the trivial character.  -/
AddChar.mulShift_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : CommMonoid M] (ψ : AddChar R M), ψ.mulShift 0 = 1
-- Mathlib.Data.Nat.Periodic
Nat.periodic_mod : ∀ (a : ℕ), Function.Periodic (fun n => n % a) a
-- Mathlib.Data.Fin.Tuple.Basic
Fin.snoc_left_injective : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} (xₙ : α (Fin.last n)), Function.Injective fun x => Fin.snoc x xₙ
-- Mathlib.Analysis.Complex.Basic
Complex.equivRealProdCLM_symm_apply_re : ∀ (a : ℝ × ℝ), (Complex.equivRealProdCLM.symm a).re = a.1
-- Mathlib.Algebra.Lie.TensorProduct
LieModule.toModuleHom.eq_1 : ∀ (R : Type u) [inst : CommRing R] (L : Type v) (M : Type w) [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M],
  LieModule.toModuleHom R L M =
    (TensorProduct.LieModule.liftLie R L L M M)
      (let __src := ↑(LieModule.toEnd R L M);
      { toLinearMap := __src, map_lie' := ⋯ })
-- Std.Time.DateTime
/-- Creates a new `DateTime` by adjusting the year to the given `year` value. The month and day remain unchanged,
and any invalid days for the new year will be handled according to the `clip` behavior.
 -/
Std.Time.DateTime.withYearClip : Std.Time.DateTime → Std.Time.Year.Offset → Std.Time.DateTime