mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
CovariantDerivative.torsion_eq_zero_iff : ∀ {𝕜 : 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] [inst_6 : CompleteSpace 𝕜] [inst_7 : CompleteSpace E]
  [inst_8 : FiniteDimensional 𝕜 E] [inst_9 : IsManifold I 2 M] (cov : CovariantDerivative I E (TangentSpace I)),
  cov.torsion = 0 ↔
    ∀ {X Y : (x : M) → TangentSpace I x} {x : M},
      MDiffAt (T% X) x → MDiffAt (T% Y) x → (↑cov Y x) (X x) - (↑cov X x) (Y x) = VectorField.mlieBracket I X Y x
-- Mathlib.Algebra.BigOperators.Finprod
finsum_mem_univ : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (f : α → M),
  ∑ᶠ (i : α) (_ : i ∈ Set.univ), f i = ∑ᶠ (i : α), f i
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The left map in the left unitality square.
 -/
CategoryTheory.Functor.LaxMonoidal.ofBifunctor.leftMapₗ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          (F : CategoryTheory.Functor C D) → F.comp (CategoryTheory.MonoidalCategory.tensorUnitLeft D) ⟶ F
-- Mathlib.Order.Category.NonemptyFinLinOrd
NonemptyFinLinOrd.dualEquiv_functor : NonemptyFinLinOrd.dualEquiv.functor = NonemptyFinLinOrd.dual
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycle.pow_eq_pow_iff : ∀ {β : Type u_3} [Finite β] {f : Equiv.Perm β},
  f.IsCycle → ∀ {a b : ℕ}, f ^ a = f ^ b ↔ ∃ x, f x ≠ x ∧ (f ^ a) x = (f ^ b) x
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.ext : ∀ {R : Type r} {inst : CommRing R} {W' : WeierstrassCurve.Jacobian R} {x y : W'.Point}, x.point = y.point → x = y
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- When `S.f = 0`, this is the canonical isomorphism `S.opcycles ≅ S.X₂`
induced by `S.pOpcycles`.  -/
CategoryTheory.ShortComplex.opcyclesIsoX₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) → [inst_2 : S.HasRightHomology] → S.f = 0 → (S.opcycles ≅ S.X₂)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
/-- The obvious map `PullbackCone f g → PushoutCocone f.unop g.unop`  -/
CategoryTheory.Limits.PullbackCone.unop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : Cᵒᵖ} →
      {f : X ⟶ Z} →
        {g : Y ⟶ Z} → CategoryTheory.Limits.PullbackCone f g → CategoryTheory.Limits.PushoutCocone f.unop g.unop
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_toList_rcc : ∀ {m n : ℕ}, (m...=n).toList.toArray = (m...=n).toArray
-- Mathlib.Analysis.RCLike.Basic
RCLike.conj_im : ∀ {K : Type u_1} [inst : RCLike K] (z : K), RCLike.im ((starRingEnd K) z) = -RCLike.im z
-- Mathlib.Algebra.Group.Irreducible.Lemmas
not_addIrreducible_nsmul : ∀ {M : Type u_2} [inst : AddMonoid M] {x : M} {n : ℕ}, n ≠ 1 → ¬AddIrreducible (n • x)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.startsWith_char_eq_false_iff_get : ∀ {c : Char} {s : String}, s.startsWith c = false ↔ ∀ (h : s.startPos ≠ s.endPos), s.startPos.get h ≠ c
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)),
  S.Exact ↔ Function.Exact ⇑(CategoryTheory.ConcreteCategory.hom S.f) ⇑(CategoryTheory.ConcreteCategory.hom S.g)
-- Mathlib.Algebra.Group.Defs
/-- A monoid is Dedekind-finite if every element with a right inverse also has a left inverse.  -/
IsDedekindFiniteMonoid.of_exists_mul_self_eq_one : ∀ (M : Type u_2) [inst : Monoid M], (∀ (x y : M), x * y = 1 → ∃ z, z * x = 1) → IsDedekindFiniteMonoid M
-- Init.Data.BitVec.Bitblast
/-- Only perform a round of shift-subtract if we have dividend bits.  -/
BitVec.DivModState.Poised.hwn_lt : ∀ {w : ℕ} {args : BitVec.DivModArgs w} {qr : BitVec.DivModState w}, BitVec.DivModState.Poised args qr → 0 < qr.wn
-- Mathlib.Analysis.Normed.Ring.Basic
nnnorm_mul_le : ∀ {α : Type u_2} [inst : NonUnitalSeminormedRing α] (a b : α), ‖a * b‖₊ ≤ ‖a‖₊ * ‖b‖₊
-- Init.Data.Array.Sort.Basic
_private.Init.Data.Array.Sort.Basic.0.Array.MergeSort.Internal.merge.go : {α : Type u_1} →
  (α → α → Bool) → (xs ys : Subarray α) → 0 < Std.Slice.size xs → 0 < Std.Slice.size ys → Array α → Array α
-- Mathlib.Topology.Maps.Basic
IsOpenMap.comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z], IsOpenMap g → IsOpenMap f → IsOpenMap (g ∘ f)
-- Std.Tactic.BVDecide.LRAT.Internal.CompactLRATCheckerSound
Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go.match_3.congr_eq_5 : ∀ {n : ℕ} (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClauseAction n) → Sort u_1)
  (step : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClauseAction n)) (h_1 : Unit → motive none)
  (h_2 : (id : ℕ) → (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints)))
  (h_3 :
    (id : ℕ) →
      (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
        (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints)))
  (h_4 :
    (id : ℕ) →
      (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
        (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
          (rupHints : Array ℕ) →
            (ratHints : Array (ℕ × Array ℕ)) →
              motive (some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints)))
  (h_5 : (ids : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.del ids))) (ids : Array ℕ),
  step = some (Std.Tactic.BVDecide.LRAT.Action.del ids) →
    (match step with
      | none => h_1 ()
      | some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints) => h_2 id rupHints
      | some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints) => h_3 id c rupHints
      | some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints) => h_4 id c pivot rupHints ratHints
      | some (Std.Tactic.BVDecide.LRAT.Action.del ids) => h_5 ids) ≍
      h_5 ids
-- Mathlib.Topology.Instances.Matrix
continuous_matrix_diag : ∀ {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace R], Continuous Matrix.diag
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.IntegrableOn.empty : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}, μ.IntegrableOn f ∅
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
CategoryTheory.Limits.IsTerminal.from_self : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (t : CategoryTheory.Limits.IsTerminal X),
  t.from X = CategoryTheory.CategoryStruct.id X
-- Mathlib.Topology.Order.IsLUB
/-- **Alias** of `IsLUB.mem_of_isClosed`. -/
IsClosed.isLUB_mem : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a : α} {s : Set α},
  IsLUB s a → s.Nonempty → IsClosed s → a ∈ s
-- Mathlib.Data.Set.Finite.Lattice
Set.map_finite_biInf : ∀ {α : Type u} {β : Type v} {F : Type u_1} {ι : Type u_2} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  [inst_2 : FunLike F α β] [InfTopHomClass F α β] {s : Set ι},
  s.Finite → ∀ (f : F) (g : ι → α), f (⨅ x ∈ s, g x) = ⨅ x ∈ s, f (g x)
-- Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
AlgebraicGeometry.weaklyEtale_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.WeaklyEtale f ↔
    autoParam (AlgebraicGeometry.Flat f) AlgebraicGeometry.WeaklyEtale.flat._autoParam ∧
      autoParam (AlgebraicGeometry.Flat (CategoryTheory.Limits.pullback.diagonal f))
        AlgebraicGeometry.WeaklyEtale.flat_diagonal._autoParam
-- Mathlib.Analysis.InnerProductSpace.Completion
UniformSpace.Completion.Continuous.inner : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {α : Type u_4} [inst_3 : TopologicalSpace α] {f g : α → UniformSpace.Completion E},
  Continuous f → Continuous g → Continuous fun x => inner 𝕜 (f x) (g x)
-- Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
AddSubmonoid.smul_mem_pointwise_smul_iff : ∀ {G : Type u_2} {A : Type u_4} [inst : AddMonoid A] [inst_1 : Group G] [inst_2 : DistribMulAction G A] {a : G}
  {S : AddSubmonoid A} {x : A}, a • x ∈ a • S ↔ x ∈ S
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
Lean.Elab.ConfigEval.EvalConfigItemHandlerKind.exact.sizeOf_spec : sizeOf Lean.Elab.ConfigEval.EvalConfigItemHandlerKind.exact = 1
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.liftEquiv_coe : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] (N : Subgroup G) [nN : N.Normal] {φ : G →* H}
  (hφ : Function.Surjective ⇑φ) (HN : N = φ.ker) (g : G), (QuotientGroup.liftEquiv N hφ HN) ↑g = φ g
-- Mathlib.Analysis.InnerProductSpace.Defs
PUnit.inner_eq_zero : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (x y : PUnit.{u_4 + 1}), inner 𝕜 x y = 0
-- Init.Data.UInt.Lemmas
UInt8.toFin_ofNatTruncate_of_lt : ∀ {n : ℕ} (hn : n < UInt8.size), (UInt8.ofNatClamp n).toFin = ⟨n, hn⟩
-- Mathlib.Data.Finset.Prod
/-- The product `s ×ˢ t` of two finsets, viewed as a subtype, is equivalent to the product of the
subtypes `s × t`. The `Finset` analogue of `Equiv.Set.prod`.  -/
Equiv.Finset.prod : {α : Type u_1} → {β : Type u_2} → (s : Finset α) → (t : Finset β) → ↥(s ×ˢ t) ≃ ↥s × ↥t
-- Mathlib.RingTheory.AdicCompletion.Functoriality
/-- If `ι` is finite, `sum` has `sumInv` as inverse.  -/
AdicCompletion.sumEquivOfFintype : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      {ι : Type u_6} →
        (M : ι → Type u_7) →
          [inst_1 : (i : ι) → AddCommGroup (M i)] →
            [inst_2 : (i : ι) → Module R (M i)] →
              [Fintype ι] →
                [DecidableEq ι] →
                  (DirectSum ι fun j => AdicCompletion I (M j)) ≃ₗ[AdicCompletion I R]
                    AdicCompletion I (DirectSum ι fun j => M j)
-- Std.Http.Internal.Char
/-- etagc = "!" / %x23-7E
; ASCII-only variant (no obs-text).
 -/
Std.Http.Internal.Char.etagc : Char → Bool
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.toSubmodule_le_toSubmodule : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (K K' : LieSubalgebra R L), K.toSubmodule ≤ K'.toSubmodule ↔ K ≤ K'
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.instIsScalarTowerRing_2 : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (P : Algebra.Extension R S)
  {R₀ : Type u_1} [inst_3 : CommRing R₀] [inst_4 : Algebra R₀ R] [inst_5 : Algebra R₀ S]
  [inst_6 : IsScalarTower R₀ R S], IsScalarTower R₀ P.Ring S
-- Mathlib.Topology.Order.Hom.Basic
/-- `id` as a `ContinuousOrderHom`.  -/
ContinuousOrderHom.id : (α : Type u_2) → [inst : TopologicalSpace α] → [inst_1 : Preorder α] → α →Co α
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
LinearMap.BilinMap.polarBilin_toQuadraticMap : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] {B : LinearMap.BilinMap R M N},
  B.toQuadraticMap.polarBilin = B + LinearMap.flip B
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.adjMatrix_mul_apply : ∀ {α : Type u_1} {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : Fintype V]
  [inst_2 : NonAssocSemiring α] (M : Matrix V V α) (v w : V),
  (SimpleGraph.adjMatrix α G * M) v w = ∑ u ∈ G.neighborFinset v, M u w
-- Mathlib.Combinatorics.Matroid.Basic
/-- **Alias** of `Matroid.IsBase.encard_sdiff_comm`. -/
Matroid.IsBase.encard_diff_comm : ∀ {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α}, M.IsBase B₁ → M.IsBase B₂ → (B₁ \ B₂).encard = (B₂ \ B₁).encard
-- Mathlib.Order.OrdContinuous
RightOrdContinuous.map_iInf : ∀ {α : Type u} {β : Type v} {ι : Sort x} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] {f : α → β},
  RightOrdContinuous f → ∀ [Nonempty ι] (g : ι → α), f (⨅ i, g i) = ⨅ i, f (g i)
-- Mathlib.Data.Sym.Basic
Sym.ofVector_cons : ∀ {α : Type u_1} {n : ℕ} (a : α) (v : List.Vector α n), Sym.ofVector (a ::ᵥ v) = a ::ₛ Sym.ofVector v
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.solveElim.sizeOf_spec : ∀ (c₁ c₂ : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.solveElim c₁ c₂) = 1 + sizeOf c₁ + sizeOf c₂
-- Mathlib.Tactic.NormNum.Result
/-- Assert that an element of a ring is equal to the coercion of some integer.  -/
Mathlib.Meta.NormNum.IsInt : {α : Type u} → [Ring α] → α → ℤ → Prop
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.hasForgetToCommRingCat : {R : Type u} → [inst : CommRing R] → CategoryTheory.HasForget₂ (CommAlgCat R) CommRingCat
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
/-- If `G` is a Galois group for `L/K` and the inertia group of `P` in `G` is a Galois group for
`L/E`, then `E` is an inertia field for `P`.
 -/
IsInertiaField.of_isGaloisGroup : ∀ (K : Type u_2) (L : Type u_3) {B : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : CommRing B] (P : Ideal B) (E : Type u_6) [inst_4 : Field E] [inst_5 : Algebra E L]
  [inst_6 : MulSemiringAction Gal(L/K) B] (G : Type u_7) [inst_7 : Group G] [Finite G] [inst_9 : MulSemiringAction G L]
  [IsGaloisGroup G K L] [inst_11 : MulSemiringAction G B] [inst_12 : Algebra B L] [IsFractionRing B L]
  [SMulDistribClass Gal(L/K) B L] [SMulDistribClass G B L] [h : IsGaloisGroup (↥(Ideal.inertia G P)) E L],
  IsInertiaField K L P E
-- Mathlib.Analysis.SpecificLimits.Normed
summable_norm_geometric_of_norm_lt_one : ∀ {R : Type u_4} [inst : NormedRing R] {r : R}, ‖r‖ < 1 → Summable fun n => ‖r ^ n‖
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coeIdeal_le_one : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {I : Ideal R}, ↑I ≤ 1
-- Mathlib.Analysis.Normed.Unbundled.FiniteExtension
Module.Basis.norm.eq_1 : ∀ {K : Type u_1} {L : Type u_2} [inst : NormedField K] [inst_1 : Ring L] [inst_2 : Algebra K L] {ι : Type u_3}
  [inst_3 : Fintype ι] [inst_4 : Nonempty ι] (B : Module.Basis ι K L) (x : L),
  B.norm x = Finset.univ.sup' ⋯ fun i => ‖(B.repr x) i‖
-- Init.Data.Int.Basic
Int.instInhabited : Inhabited ℤ
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.atLeastFn : ℕ → Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.Data.Real.Basic
Real.cauchy_ratCast : ∀ (q : ℚ), (↑q).cauchy = ↑q
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.mk.inj : ∀ {α : Type u_2} {E : Set α} {Indep : Set α → Prop} {indep_empty : Indep ∅}
  {indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I}
  {indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)}
  {indep_maximal : ∀ X ⊆ E, Matroid.ExistsMaximalSubsetProperty Indep X}
  {subset_ground : ∀ (I : Set α), Indep I → I ⊆ E} {E_1 : Set α} {Indep_1 : Set α → Prop} {indep_empty_1 : Indep_1 ∅}
  {indep_subset_1 : ∀ ⦃I J : Set α⦄, Indep_1 J → I ⊆ J → Indep_1 I}
  {indep_aug_1 :
    ∀ ⦃I B : Set α⦄, Indep_1 I → ¬Maximal Indep_1 I → Maximal Indep_1 B → ∃ x ∈ B \ I, Indep_1 (insert x I)}
  {indep_maximal_1 : ∀ X ⊆ E_1, Matroid.ExistsMaximalSubsetProperty Indep_1 X}
  {subset_ground_1 : ∀ (I : Set α), Indep_1 I → I ⊆ E_1},
  { E := E, Indep := Indep, indep_empty := indep_empty, indep_subset := indep_subset, indep_aug := indep_aug,
        indep_maximal := indep_maximal, subset_ground := subset_ground } =
      { E := E_1, Indep := Indep_1, indep_empty := indep_empty_1, indep_subset := indep_subset_1,
        indep_aug := indep_aug_1, indep_maximal := indep_maximal_1, subset_ground := subset_ground_1 } →
    E = E_1 ∧ Indep = Indep_1
-- Mathlib.GroupTheory.OrderOfElement
/-- The equivalence between `Submonoid.powers` of two elements `x, y` of the same order, mapping
`x ^ i` to `y ^ i`.  -/
powersEquivPowers : {G : Type u_1} →
  [inst : LeftCancelMonoid G] →
    [Finite G] → {x y : G} → orderOf x = orderOf y → ↥(Submonoid.powers x) ≃ ↥(Submonoid.powers y)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_insert_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited β] {k : α} {v : β}, Std.DHashMap.Const.get! (m.insert k v) k = v
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.toReal_eq_pi_div_two_iff : ∀ {θ : Real.Angle}, θ.toReal = Real.pi / 2 ↔ θ = ↑(Real.pi / 2)
-- Mathlib.AlgebraicGeometry.Geometrically.Connected
AlgebraicGeometry.instGeometricallyConnectedMorphismRestrict : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (V : S.Opens) [AlgebraicGeometry.GeometricallyConnected f],
  AlgebraicGeometry.GeometricallyConnected (f ∣_ V)
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
/-- A ring satisfying `StrongRankCondition` (such as a `DivisionRing`) is one-dimensional as a
module over itself.  -/
Module.finrank_self : ∀ (R : Type u) [inst : Semiring R] [StrongRankCondition R], Module.finrank R R = 1
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Over.prodLeftIsoPullback_inv_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (Y Z : CategoryTheory.Over X)
  [inst_1 : CategoryTheory.Limits.HasPullback Y.hom Z.hom] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Y Z],
  CategoryTheory.CategoryStruct.comp (Y.prodLeftIsoPullback Z).inv
      (CategoryTheory.Over.Hom.left CategoryTheory.Limits.prod.fst) =
    CategoryTheory.Limits.pullback.fst Y.hom Z.hom
-- Mathlib.Topology.Separation.Basic
T1Space.mk : ∀ {X : Type u} [inst : TopologicalSpace X], (∀ (x : X), IsClosed {x}) → T1Space X
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.formatPartWithDate : Std.Time.DateFormat → Std.Time.DateTime → Std.Time.FormatPart → String
-- Mathlib.Analysis.Convex.Gauge
setOfPred_gauge_le_eq : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} {a : ℝ},
  Convex ℝ s → 0 ∈ s → Absorbent ℝ s → 0 ≤ a → {x | gauge s x ≤ a} = ⋂ r, ⋂ (_ : a < r), r • s
-- Mathlib.Algebra.Group.Opposite
MulOpposite.semiconjBy_unop : ∀ {α : Type u_1} [inst : Mul α] {a x y : αᵐᵒᵖ},
  SemiconjBy (MulOpposite.unop a) (MulOpposite.unop y) (MulOpposite.unop x) ↔ SemiconjBy a x y
-- Mathlib.CategoryTheory.Monad.Basic
/-- Transport a monad structure on a functor along an isomorphism of functors.  -/
CategoryTheory.Monad.transport : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F : CategoryTheory.Functor C C} → (T : CategoryTheory.Monad C) → (T.toFunctor ≅ F) → CategoryTheory.Monad C
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- The essential image of a full and faithful functor between cartesian-monoidal categories is the
same on additive group objects as on objects.  -/
CategoryTheory.Functor.essImage_mapAddGrp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] [F.Full] [F.Faithful] {G : CategoryTheory.AddGrp D},
  F.mapAddGrp.essImage G ↔ F.essImage G.X
-- Lean.Elab.InfoTree.Types
/-- The piece of syntax that the elaborator created this info for.
Note that this also implicitly stores the code position in the syntax's SourceInfo.  -/
Lean.Elab.ElabInfo.stx : Lean.Elab.ElabInfo → Lean.Syntax
-- Mathlib.GroupTheory.Complement
AddSubgroup.isComplement_univ_right : ∀ {G : Type u_1} [inst : AddGroup G] {S : Set G}, AddSubgroup.IsComplement S Set.univ ↔ ∃ g, S = {g}
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.sInf_toSubsemiring : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : Set (Subalgebra R A)), (sInf S).toSubsemiring = sInf (Subalgebra.toSubsemiring '' S)
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- Given a multilinear map `f` on `n` variables (parameterized by `Fin n`) and a subset `s` of `k`
of these variables, one gets a new multilinear map on `Fin k` by varying these variables, and fixing
the other ones equal to a given value `z`. It is denoted by `f.restr s hk z`, where `hk` is a
proof that the cardinality of `s` is `k`. The implicit identification between `Fin k` and `s` that
we use is the canonical (increasing) bijection.  -/
MultilinearMap.restr : {R : Type uR} →
  {M₂ : Type v₂} →
    {M' : Type v'} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M₂] →
          [inst_2 : AddCommMonoid M'] →
            [inst_3 : Module R M₂] →
              [inst_4 : Module R M'] →
                {k n : ℕ} →
                  MultilinearMap R (fun x => M') M₂ →
                    (s : Finset (Fin n)) → s.card = k → M' → MultilinearMap R (fun x => M') M₂
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.submatrixEquivInvertibleEquivInvertible_symm_apply : ∀ {m : Type u} {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α]
  [inst_3 : Fintype m] [inst_4 : DecidableEq m] (A : Matrix m m α) (e₁ e₂ : n ≃ m) (x : Invertible A),
  (A.submatrixEquivInvertibleEquivInvertible e₁ e₂).symm x = A.submatrixEquivInvertible e₁ e₂
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.homologyMap_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [inst_2 : K.HasHomology i],
  HomologicalComplex.homologyMap (CategoryTheory.CategoryStruct.id K) i =
    CategoryTheory.CategoryStruct.id (K.homology i)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.zero_lt_one : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] [inst_1 : LE α] [inst_2 : LT α] [Std.LawfulOrderLT α]
  [inst_4 : Std.IsPreorder α] [Lean.Grind.OrderedRing α] (ctx : Lean.Grind.Linarith.Context α)
  (p : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.zero_lt_one_cert p = true →
    Lean.Grind.Linarith.Var.denote ctx 0 = One.one → Lean.Grind.Linarith.Poly.denote' ctx p < 0
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquiv.mk_coe : ∀ {A : Type u_1} {B : Type u_2} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B] [inst_4 : Star A]
  [inst_5 : Star B] (e : A ≃⋆+* B) (e' : B → A) (h₁ : Function.LeftInverse e' ⇑e) (h₂ : Function.RightInverse e' ⇑e)
  (h₃ :
    ∀ (x y : A),
      { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x * y) =
        { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x *
          { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y)
  (h₄ :
    ∀ (x y : A),
      { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x + y) =
        { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x +
          { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y)
  (h₅ :
    ∀ (a : A),
      { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun (star a) =
        star ({ toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun a)),
  { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, map_star' := h₅ } = e
-- Mathlib.Order.CountableSupClosed
countableInfClosed_preimage_ofDual : ∀ {α : Type u_2} [inst : LE α] {s : Set α}, CountableInfClosed (⇑OrderDual.ofDual ⁻¹' s) ↔ CountableSupClosed s
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.isEmpty_filter_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  {f : α → β → Bool},
  t.WF →
    ((Std.DTreeMap.Raw.filter f t).isEmpty = true ↔
      ∀ (k : α) (h : k ∈ t), f (t.getKey k h) (Std.DTreeMap.Raw.Const.get t k h) = false)