mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Lemmas.Pattern.Find.Char
String.Pos.find?_char_eq_some_iff : ∀ {c : Char} {s : String} {pos pos' : s.Pos},
  pos.find? c = some pos' ↔
    pos ≤ pos' ∧
      (∃ (h : pos' ≠ s.endPos), pos'.get h = c) ∧
        ∀ (pos'' : s.Pos), pos ≤ pos'' → ∀ (h' : pos'' < pos'), pos''.get ⋯ ≠ c
-- Mathlib.Data.ENNReal.Real
ENNReal.ofReal_lt_ofReal_iff' : ∀ {p q : ℝ}, ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q ∧ 0 < q
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.getElem?_toList_eq : ∀ {α : Type u} {r : Std.Rii α} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_4 : Std.Rxi.IsAlwaysFinite α] {i : ℕ}, r.toList[i]? = Std.PRange.least?.bind (Std.PRange.succMany? i)
-- Mathlib.Computability.Reduce
ManyOneDegree.le_add_left : ∀ (d₁ d₂ : ManyOneDegree), d₁ ≤ d₁ + d₂
-- Mathlib.Algebra.Order.Star.Basic
IsSelfAdjoint.iff_of_le : ∀ {R : Type u_1} [inst : NonUnitalRing R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R] {a b : R},
  a ≤ b → (IsSelfAdjoint a ↔ IsSelfAdjoint b)
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- **Alias** of `Bundle.Trivialization.localFrameCoeff_congr`.

---

The representation of `s` in a local frame at `x` only depends on `s` at `x`.  -/
Bundle.Trivialization.localFrame_coeff_congr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] [inst_13 : VectorBundle 𝕜 F V] {ι : Type u_7}
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_14 : MemTrivializationAtlas e] (b : Module.Basis ι 𝕜 F)
  [inst_15 : ContMDiffVectorBundle 1 F V I] {x : M} {s s' : (x : M) → V x} {i : ι},
  s x = s' x →
    (Bundle.Trivialization.localFrameCoeff I e b i x) (s x) = (Bundle.Trivialization.localFrameCoeff I e b i x) (s' x)
-- Aesop.Rule.Name
_private.Aesop.Rule.Name.0.Aesop.RuleName.Json.mk.inj : ∀ {name : Lean.Name} {builder : Aesop.BuilderName} {phase : Aesop.PhaseName} {scope : Aesop.ScopeName}
  {rendered : String} {name_1 : Lean.Name} {builder_1 : Aesop.BuilderName} {phase_1 : Aesop.PhaseName}
  {scope_1 : Aesop.ScopeName} {rendered_1 : String},
  { name := name, builder := builder, phase := phase, scope := scope, rendered := rendered } =
      { name := name_1, builder := builder_1, phase := phase_1, scope := scope_1, rendered := rendered_1 } →
    name = name_1 ∧ builder = builder_1 ∧ phase = phase_1 ∧ scope = scope_1 ∧ rendered = rendered_1
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.basisRepr_apply : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_8} [inst_5 : Fintype ι] {v : Module.Basis ι R M}
  (Q : QuadraticMap R M N) (w : ι → R), (Q.basisRepr v) w = Q (∑ i, w i • v i)
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.assemble₃Unchecked.eq_1 : ∀ (w x y : UInt8),
  ByteArray.utf8DecodeChar?.assemble₃Unchecked w x y =
    (w &&& 15).toUInt32 <<< 12 ||| (x &&& 63).toUInt32 <<< 6 ||| (y &&& 63).toUInt32
-- Lean.Compiler.IR.Basic
Lean.IR.CtorInfo.name : Lean.IR.CtorInfo → Lean.Name
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- A cylinder set on `U` is the `Set.pi` over `U` of the singletons `{x i}`,
viewed as a subset of `G → A`. Equivalently, it is the preimage of that product
of singletons in `U → A` under the restriction map `(G → A) → (U → A)`.  -/
SymbolicDynamics.FullShift.cylinder_eq_set_pi : ∀ {A : Type u_1} {G : Type u_2} (U : Finset G) (x : G → A),
  SymbolicDynamics.FullShift.cylinder U x = (↑U).pi fun i => {x i}
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.xPrevIso_comp_dTo : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i j : ι}
  (r : c.Rel i j), CategoryTheory.CategoryStruct.comp (C.xPrevIso r).inv (C.dTo j) = C.d i j
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.val_smul : ∀ {R : Type u} {M : Type v} [inst : SMul R M] {p : SubMulAction R M} (r : R) (x : ↥p), ↑(r • x) = r • ↑x
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.num.sizeOf_spec : ∀ (k : ℤ), sizeOf (Lean.Grind.CommRing.Poly.num k) = 1 + sizeOf k
-- Mathlib.Condensed.Light.Sequence
_private.Mathlib.Condensed.Light.Sequence.0.InternalProjectivityProof.fibres.eq_1 : ∀ {S : Type u_1} {T : Type u_2} {X : Type u_3} (π : T → S × Option X) (σ : Option X → S → T),
  InternalProjectivityProof.fibres✝ π σ = {t | (π t).2 = none} ∪ ⋃ x, Set.range (σ (some x))
-- Mathlib.RingTheory.SimpleRing.Field
IsSimpleRing.isField_center : ∀ (A : Type u_1) [inst : Ring A] [IsSimpleRing A], IsField ↥(Subring.center A)
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
ComplexShape.Embedding.AreComplementary.Boundary.snd : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} {ac : e₁.AreComplementary e₂} {i₁ : ι₁} {i₂ : ι₂},
  ac.Boundary i₁ i₂ → e₂.BoundaryGE i₂
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- The condition that a property of morphisms is stable by filtered colimits.  -/
CategoryTheory.MorphismProperty.IsStableUnderFilteredColimits : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → Prop
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.getEntryGE?.go : {α : Type u} →
  {β : α → Type v} → [Ord α] → α → Option ((a : α) × β a) → Std.DTreeMap.Internal.Impl α β → Option ((a : α) × β a)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.instMonoidalOppositeFunctorOpOpEquivalence : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → (CategoryTheory.opOpEquivalence C).functor.Monoidal
-- Mathlib.AlgebraicTopology.SimplicialSet.NonsingularColimit
SSet.Nonsingular.iso.congr_simp : ∀ {X : SSet} [inst : X.Nonsingular] {n : ℕ} (x : X.obj (Opposite.op { len := n })) (hx : x ∈ X.nonDegenerate n),
  SSet.Nonsingular.iso x hx = SSet.Nonsingular.iso x hx
-- Mathlib.LinearAlgebra.LinearDisjoint
Submodule.LinearDisjoint.of_subsingleton_top : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M N : Submodule R S}
  [Subsingleton S], M.LinearDisjoint N
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Path.Balanced.below.redL : ∀ {c₀ : RBTree.RBColor} {n₀ : ℕ} {α : Type u_1}
  {motive :
    (a : RBTree.RBNode.Path α) →
      (a_1 : RBTree.RBColor) → (a_2 : ℕ) → RBTree.RBNode.Path.Balanced c₀ n₀ a a_1 a_2 → Prop}
  {y : RBTree.RBNode α} {n : ℕ} {parent : RBTree.RBNode.Path α} {v : α} (a : y.Balanced RBTree.RBColor.black n)
  (a_1 : RBTree.RBNode.Path.Balanced c₀ n₀ parent RBTree.RBColor.red n),
  RBTree.RBNode.Path.Balanced.below a_1 → motive parent RBTree.RBColor.red n a_1 → RBTree.RBNode.Path.Balanced.below ⋯
-- Mathlib.AlgebraicTopology.ModelCategory.Over
HomotopicalAlgebra.instFibrationLeftOfOver : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (S : C) [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C]
  {X Y : CategoryTheory.Over S} (f : X ⟶ Y) [HomotopicalAlgebra.Fibration f],
  HomotopicalAlgebra.Fibration (CategoryTheory.Over.Hom.left f)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.coe_mk : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s : TopologicalSpace.Compacts α) (h : s.carrier.Nonempty),
  ↑{ toCompacts := s, nonempty' := h } = ↑s
-- Mathlib.Algebra.Category.MonCat.Basic
/-- The category of additive commutative monoids and monoid morphisms.  -/
AddCommMonCat : Type (u + 1)
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.ofHom_id : ∀ {R : Type u} [inst : CommRing R],
  CommRingCat.ofHom (RingHom.id R) = CategoryTheory.CategoryStruct.id (CommRingCat.of R)
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.ofArrows_comp_eq_of_surjective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {ι : Type u_1} {σ : Type u_2} {Y : ι → C}
  (f : (i : ι) → Y i ⟶ X) {a : σ → ι},
  Function.Surjective a →
    (CategoryTheory.Presieve.ofArrows (Y ∘ a) fun i => f (a i)) = CategoryTheory.Presieve.ofArrows Y f
-- Mathlib.Algebra.Star.Subalgebra
/-- Embedding of a subalgebra into the algebra.  -/
StarSubalgebra.subtype : {R : Type u_2} →
  {A : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : Semiring A] →
          [inst_3 : StarRing A] →
            [inst_4 : Algebra R A] → [inst_5 : StarModule R A] → (S : StarSubalgebra R A) → ↥S →⋆ₐ[R] A
-- Mathlib.Topology.Algebra.Group.Basic
Filter.map_divLeft_nhdsGT : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : CommGroup H] [IsTopologicalGroup H] [inst_3 : PartialOrder H]
  [IsOrderedMonoid H] {c a : H},
  Filter.map (fun x => c / x) (nhdsWithin a (Set.Ioi a)) = nhdsWithin (c / a) (Set.Iio (c / a))
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.condIndepFun_const_left : ∀ {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {mβ : MeasurableSpace β}
  {mβ' : MeasurableSpace β'} (c : β) (X : Ω → β'), ProbabilityTheory.CondIndepFun m' hm' (fun x => c) X μ
-- Mathlib.SetTheory.ZFC.Ordinal
Ordinal.toPSet.eq_def : ∀ (o : Ordinal.{u}), o.toPSet = PSet.mk o.ToType fun a => (↑a.toOrd).toPSet
-- Mathlib.Algebra.Ring.Int.Parity
Int.two_mul_ediv_two_add_one_of_odd : ∀ {n : ℤ}, Odd n → 2 * (n / 2) + 1 = n
-- Mathlib.Algebra.Order.Module.Defs
neg_of_smul_pos_right : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β]
  [inst_3 : LinearOrder α] [inst_4 : LinearOrder β] [PosSMulMono α β] [SMulPosMono α β], 0 < a • b → a ≤ 0 → b < 0
-- Mathlib.Topology.Algebra.Monoid
/-- **Alias** of `isClosed_setOfPred_map_add`. -/
isClosed_setOf_map_add : ∀ (M₁ : Type u_6) (M₂ : Type u_7) [inst : TopologicalSpace M₂] [T2Space M₂] [inst_2 : Add M₁] [inst_3 : Add M₂]
  [ContinuousAdd M₂], IsClosed {f | ∀ (x y : M₁), f (x + y) = f x + f y}
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.prod_ne_zero : ∀ {ι : Type u_1} (f : ι → Cardinal.{u_2}), Cardinal.prod f ≠ 0 ↔ ∀ (i : ι), f i ≠ 0
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.homotopicTo : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} [inst_1 : DecidableEq N] (i : N)
  {p q : ↑(GenLoop N X x)}, GenLoop.Homotopic p q → Path.Homotopic (GenLoop.toLoop i p) (GenLoop.toLoop i q)
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.revMatchAt?_eq_revMatchAt?_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.revMatchAt? p pos = String.Slice.Pattern.Model.revMatchAt? (fun x => decide (p x)) pos
-- Init.Data.Iterators.Lemmas.Combinators.ULift
Std.Iter.toListRev_uLift : ∀ {α β : Type u} [inst : Std.Iterator α Id β] {it : Std.Iter β} [Std.Iterators.Finite α Id],
  it.uLift.toListRev = List.map ULift.up it.toListRev
-- Mathlib.Data.Nat.Digits.Defs
Nat.digits.eq_2 : Nat.digits 1 = Nat.digitsAux1
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
CategoryTheory.MorphismProperty.instIsIsoMapS : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] {X Y : C} (z : W.LeftFraction₂ X Y),
  CategoryTheory.IsIso (L.map z.s)
-- Mathlib.Algebra.Order.Antidiag.Pi
Finset.piAntidiag.eq_1 : ∀ {ι : Type u_1} {μ : Type u_2} [inst : DecidableEq ι] [inst_1 : AddCommMonoid μ] [inst_2 : Finset.HasAntidiagonal μ]
  [inst_3 : DecidableEq μ] (s : Finset ι) (n : μ),
  s.piAntidiag n =
    Trunc.lift
      (fun e =>
        Finset.map { toFun := fun f i => if hi : i ∈ s then f (e ⟨i, hi⟩) else 0, inj' := ⋯ }
          (Finset.finAntidiagonal s.card n))
      ⋯ (Fintype.truncEquivFinOfCardEq ⋯)
-- Mathlib.Algebra.Module.LinearMap.End
/-- Each element of the semiring defines a module endomorphism.

This is a stronger version of `DistribMulAction.toModuleEnd`.  -/
Module.toModuleEnd : (R : Type u_1) →
  {S : Type u_3} →
    (M : Type u_4) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : Semiring S] → [inst_4 : Module S M] → [SMulCommClass S R M] → S →+* Module.End R M
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isNClique_one : ∀ {α : Type u_1} {G : SimpleGraph α} {s : Finset α}, G.IsNClique 1 s ↔ ∃ a, s = {a}
-- Mathlib.Data.FinEnum
FinEnum.empty : FinEnum Empty
-- Mathlib.Data.Finset.Card
Finset.card_le_one_iff_subsingleton_coe : ∀ {α : Type u_1} {s : Finset α}, s.card ≤ 1 ↔ Subsingleton ↥s
-- Mathlib.RingTheory.Nullstellensatz
/-- The point in the prime spectrum associated to a given point  -/
MvPolynomial.pointToPoint : {k : Type u_1} →
  {K : Type u_2} →
    [inst : Field k] → [inst_1 : Field K] → [Algebra k K] → {σ : Type u_3} → (σ → K) → PrimeSpectrum (MvPolynomial σ k)
-- Init.Data.Sum.Lemmas
_private.Init.Data.Sum.Lemmas.0.Sum.getRight?.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : α ⊕ β → Sort u_3) (val : α) (h_1 : (b : β) → motive (Sum.inr b))
  (h_2 : (val : α) → motive (Sum.inl val)),
  (match Sum.inl val with
    | Sum.inr b => h_1 b
    | Sum.inl val => h_2 val) =
    h_2 val
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_modify : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] (h : t.WF) {k k' : α} {f : β k → β k}
  {hc : k' ∈ Std.DTreeMap.Internal.Impl.modify k f t},
  (Std.DTreeMap.Internal.Impl.modify k f t).get k' hc =
    if heq : compare k k' = Ordering.eq then cast ⋯ (f (t.get k ⋯)) else t.get k' ⋯
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- A map of 2-truncated simplicial sets induces a functor between homotopy categories.  -/
SSet.Truncated.mapHomotopyCategory : {V W : SSet.Truncated 2} → (V ⟶ W) → CategoryTheory.Functor V.HomotopyCategory W.HomotopyCategory
-- Mathlib.Algebra.Star.Subsemiring
StarSubsemiring.mk.inj : ∀ {R : Type v} {inst : NonAssocSemiring R} {inst_1 : Star R} {toSubsemiring : Subsemiring R}
  {star_mem' : ∀ {a : R}, a ∈ toSubsemiring.carrier → star a ∈ toSubsemiring.carrier} {toSubsemiring_1 : Subsemiring R}
  {star_mem'_1 : ∀ {a : R}, a ∈ toSubsemiring_1.carrier → star a ∈ toSubsemiring_1.carrier},
  { toSubsemiring := toSubsemiring, star_mem' := star_mem' } =
      { toSubsemiring := toSubsemiring_1, star_mem' := star_mem'_1 } →
    toSubsemiring = toSubsemiring_1
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_iff_unop : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J] (Q : CategoryTheory.ObjectProperty Cᵒᵖ),
  Q.IsClosedUnderColimitsOfShape J ↔ Q.unop.IsClosedUnderLimitsOfShape Jᵒᵖ
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.coe_add : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (s : NonUnitalSubsemiring R) (x y : ↥s), ↑(x + y) = ↑x + ↑y
-- Init.Data.Nat.Lemmas
Nat.min_add_left_self : ∀ {a b : ℕ}, min a (b + a) = a
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_le_lpNorm_add_lpNorm_sub : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f g : α → E},
  MeasureTheory.MemLp g p μ →
    1 ≤ p → MeasureTheory.lpNorm f p μ ≤ MeasureTheory.lpNorm g p μ + MeasureTheory.lpNorm (g - f) p μ
-- Batteries.Data.Array.Basic
/-- Check whether `xs` and `ys` are equal as sets, i.e. they contain the same
elements when disregarding order and duplicates. `O(n*m)`! If your element type
has an `Ord` instance, it is asymptotically more efficient to sort the two
arrays, remove duplicates and then compare them elementwise.
 -/
Array.equalSet : {α : Type u_1} → [BEq α] → Array α → Array α → Bool
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_maxKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = false → ∀ {fallback : α}, t.getKeyD t.maxKey! fallback = t.maxKey!
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
/-- The closure of the image of a closed submodule under a continuous linear map is a closed
submodule.

`ClosedSubmodule.map f` is left-adjoint to `ClosedSubmodule.comap f`.
See `ClosedSubmodule.gc_map_comap`.  -/
ClosedSubmodule.map : {R : Type u_2} →
  {M : Type u_3} →
    {N : Type u_4} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : TopologicalSpace M] →
            [inst_3 : Module R M] →
              [inst_4 : AddCommMonoid N] →
                [inst_5 : TopologicalSpace N] →
                  [inst_6 : Module R N] →
                    [ContinuousAdd N] →
                      [ContinuousConstSMul R N] → (M →L[R] N) → ClosedSubmodule R M → ClosedSubmodule R N
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.canonicalEmbedding.latticeBasis_apply : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (i : Module.Free.ChooseBasisIndex ℤ (NumberField.RingOfIntegers K)),
  (NumberField.canonicalEmbedding.latticeBasis K) i =
    (NumberField.canonicalEmbedding K) ((NumberField.integralBasis K) i)
-- Mathlib.Dynamics.FixedPoints.Defs
Function.mem_fixedPoints_iff : ∀ {α : Type u_2} {f : α → α} {x : α}, x ∈ Function.fixedPoints f ↔ f x = x
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.ProjectiveResolution.ofComplex_d_1_0 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.EnoughProjectives C] (Z : C),
  (CategoryTheory.ProjectiveResolution.ofComplex Z).d 1 0 = CategoryTheory.Projective.d (CategoryTheory.Projective.π Z)
-- Mathlib.Topology.Path
/-- Continuous path connecting two points `x` and `y` in a topological space  -/
Path : {X : Type u_1} → [TopologicalSpace X] → X → X → Type u_1
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.mul_coeff_zero : ∀ {R : Type u} [inst : Semiring R] (p q : Polynomial R), (p * q).coeff 0 = p.coeff 0 * q.coeff 0
-- Lean.Elab.PreDefinition.WF.Eqns
Lean.Elab.WF.instInhabitedEqnInfo : Inhabited Lean.Elab.WF.EqnInfo
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.mem_range_embedding_iff : ∀ {n : ℕ} (c : Composition n) {j : Fin n} {i : Fin c.length},
  j ∈ Set.range ⇑(c.embedding i) ↔ c.sizeUpTo ↑i ≤ ↑j ∧ ↑j < c.sizeUpTo (↑i).succ
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.coe_comp_lattice_hom : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : Lattice γ]
  [inst_3 : BoundedOrder α] [inst_4 : BoundedOrder β] [inst_5 : BoundedOrder γ] (f : BoundedLatticeHom β γ)
  (g : BoundedLatticeHom α β),
  { toFun := ⇑(f.comp g), map_sup' := ⋯, map_inf' := ⋯ } =
    { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯ }.comp { toFun := ⇑g, map_sup' := ⋯, map_inf' := ⋯ }
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndepSets.ae_isProbabilityMeasure : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {π : ι → Set (Set Ω)},
  ProbabilityTheory.Kernel.iIndepSets π κ μ → ∀ᵐ (a : α) ∂μ, MeasureTheory.IsProbabilityMeasure (κ a)
-- Mathlib.Topology.Algebra.ConstMulAction
Homeomorph.vadd_apply : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : AddGroup G] [inst_2 : AddAction G α]
  [inst_3 : ContinuousConstVAdd G α] (γ : G) (x : α), (Homeomorph.vadd γ) x = γ +ᵥ x
-- Std.Data.ExtHashMap.Basic
/-- Removes the mapping for the given key if it exists.  -/
Std.ExtHashMap.erase : {α : Type u} →
  {β : Type v} →
    {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Std.ExtHashMap α β → α → Std.ExtHashMap α β
-- Mathlib.CategoryTheory.Subfunctor.Equalizer
CategoryTheory.Subfunctor.mem_equalizer_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F₁ F₂ : CategoryTheory.Functor C (Type w)}
  {A : CategoryTheory.Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) {i : C} (x : A.toFunctor.obj i),
  ↑x ∈ (CategoryTheory.Subfunctor.equalizer f g).obj i ↔
    (CategoryTheory.ConcreteCategory.hom (f.app i)) x = (CategoryTheory.ConcreteCategory.hom (g.app i)) x
-- Mathlib.Analysis.InnerProductSpace.PiL2
InnerProductSpace.toMatrix_rankOne : ∀ {𝕜 : Type u_7} {E : Type u_8} {F : Type u_9} {ι : Type u_10} {ι' : Type u_11} [inst : RCLike 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : Finite ι] [inst_6 : Fintype ι'] [inst_7 : DecidableEq ι'] (x : E) (y : F)
  (b : Module.Basis ι 𝕜 E) (b' : OrthonormalBasis ι' 𝕜 F),
  (LinearMap.toMatrix b'.toBasis b) ↑(((InnerProductSpace.rankOne 𝕜) x) y) =
    Matrix.vecMulVec (⇑(b.repr x)) (star (b'.repr y).ofLp)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α]
  {l : List ((a : α) × β a)} {k : α} {fallback : β k},
  (List.map Sigma.fst l).contains k = false → (m.insertMany l).getD k fallback = m.getD k fallback
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Connected.of_subsingleton : ∀ {V : Type u} {G : SimpleGraph V} [Nonempty V] [Subsingleton V], G.Connected
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.unop_whiskerLeft_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E]
  {H : CategoryTheory.Functor Eᵒᵖ Cᵒᵖ} (α : F ⟶ G) {Z : CategoryTheory.Functor E D} (h : (H.comp F).unop ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.unop (H.whiskerLeft α)) h =
    CategoryTheory.CategoryStruct.comp (H.unopComp G).hom
      (CategoryTheory.CategoryStruct.comp (H.unop.whiskerLeft (CategoryTheory.NatTrans.unop α))
        (CategoryTheory.CategoryStruct.comp (H.unopComp F).inv h))
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
secondCountableTopologyEither_of_left : ∀ (α : Type u_6) (β : Type u_7) [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [SecondCountableTopology α],
  SecondCountableTopologyEither α β
-- Lean.Meta.Sym.MaxFVar
_private.Lean.Meta.Sym.MaxFVar.0.Lean.Meta.Sym.max : Option Lean.FVarId → Option Lean.FVarId → Lean.MetaM (Option Lean.FVarId)
-- Init.Notation
/-- `a &&& b` computes the bitwise AND of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `&&&` in identifiers is `and`. -/
«term_&&&_» : Lean.TrailingParserDescr
-- Mathlib.Analysis.Calculus.ContDiff.Deriv
ContDiff.iterate_deriv' : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (n k : ℕ) {f : 𝕜 → F}, ContDiff 𝕜 (↑(n + k)) f → ContDiff 𝕜 (↑n) (deriv^[k] f)
-- Mathlib.Data.Stream.Init
Stream'.get_interleave_left : ∀ {α : Type u} (n : ℕ) (s₁ s₂ : Stream' α), (s₁ ⋈ s₂).get (2 * n) = s₁.get n
-- Mathlib.Data.Real.Sign
Real.sign_mul_pos_of_ne_zero : ∀ (r : ℝ), r ≠ 0 → 0 < r.sign * r
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
/-- Constructor for `Fix F`  -/
MvQPF.Fix.mk : {n : ℕ} →
  {F : TypeVec.{u} (n + 1) → Type u} → [q : MvQPF F] → {α : TypeVec.{u} n} → F (α ::: MvQPF.Fix F α) → MvQPF.Fix F α