mathlib-initiative/mathlib-types huggingface dataset:
-- Qq.Match
Qq.Impl.makeMatchCode : {v : Lean.Level} →
  {γ : Q(Type)} →
    {m : Q(Type → Type v)} →
      Q(MonadLiftT Lean.MetaM «$m») →
        Q(Bind «$m») →
          List Qq.Impl.PatVarDecl →
            (uTy : Q(Lean.Level)) →
              (ty : Q(Q(Sort «$uTy»))) →
                Q(Q(«$$ty»)) →
                  Q(Q(«$$ty»)) →
                    Q(«$m» «$γ») →
                      Lean.Expr → (Lean.Expr → Lean.Elab.TermElabM Q(«$m» «$γ»)) → Lean.Elab.TermElabM Q(«$m» «$γ»)
-- Mathlib.Probability.Distributions.Binomial
_private.Mathlib.Probability.Distributions.Binomial.0.ProbabilityTheory.integral_of_hasLaw_binomial : {Ω : Type u_2} →
  {m : MeasurableSpace Ω} →
    {P : MeasureTheory.Measure Ω} →
      {n : ℕ} →
        {p : ↑unitInterval} →
          {X : Ω → ℝ} →
            ProbabilityTheory.HasLaw X (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.binomial n p)) P →
              ProofWanted (∫ (x : Ω), X x ∂P = ↑p * ↑n)
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegral_smul : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F}
  {γ : Path a b} {𝕝 : Type u_4} [inst_5 : RCLike 𝕝] [inst_6 : NormedSpace 𝕝 F] [inst_7 : SMulCommClass 𝕜 𝕝 F] {c : 𝕝},
  curveIntegral (c • ω) γ = c • curveIntegral ω γ
-- Mathlib.RingTheory.NonUnitalSubring.Defs
/-- A non-unital subring of a non-unital ring inherits a non-unital ring structure  -/
NonUnitalSubringClass.toNonUnitalRing : {S : Type v} →
  {R : Type u_1} →
    [inst : NonUnitalRing R] → [inst_1 : SetLike S R] → [NonUnitalSubringClass S R] → (s : S) → NonUnitalRing ↥s
-- Init.Data.BitVec.Basic
BitVec.ofBool_false : BitVec.ofBool false = 0
-- Mathlib.LinearAlgebra.TensorProduct.Map
/-- `LinearEquiv.rTensor M f : N₁ ⊗ M ≃ₗ N₂ ⊗ M` is the natural linear equivalence
induced by `f : N₁ ≃ₗ N₂`.  -/
LinearEquiv.rTensor : {R : Type u_1} →
  [inst : CommSemiring R] →
    (M : Type u_7) →
      {N : Type u_8} →
        {P : Type u_9} →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid N] →
              [inst_3 : AddCommMonoid P] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : Module R P] → (N ≃ₗ[R] P) → TensorProduct R N M ≃ₗ[R] TensorProduct R P M
-- Std.Data.Iterators.Combinators.Monadic.DropWhile
Std.Iterators.Types.DropWhile.PlausibleStep.done : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β]
  {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)} {it : Std.IterM m β},
  it.internalState.inner.IsPlausibleStep Std.IterStep.done →
    Std.Iterators.Types.DropWhile.PlausibleStep it Std.IterStep.done
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `IsAddTorsion.module_of_torsion`.

---

A module whose scalars are torsion is torsion.  -/
AddMonoid.IsTorsion.module_of_torsion : ∀ (R : Type u_3) (M : Type u_4) [inst : AddCommMonoid M] [inst_1 : Semiring R] [Module R M],
  IsAddTorsion R → IsAddTorsion M
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigOWith_self_const_mul : ∀ {α : Type u_1} {S : Type u_17} [inst : NormedRing S] [NormMulClass S] {c : S},
  c ≠ 0 → ∀ (f : α → S) (l : Filter α), Asymptotics.IsBigOWith ‖c‖⁻¹ l f fun x => c * f x
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.piEquivPiSubtypeProd_apply : ∀ {ι : Type u_7} (p : ι → Prop) [inst : DecidablePred p] (Y : ι → Type u_8)
  [inst_1 : (i : ι) → NonUnitalNonAssocSemiring (Y i)] (f : (i : ι) → Y i),
  (RingEquiv.piEquivPiSubtypeProd p Y) f = (fun x => f ↑x, fun x => f ↑x)
-- Mathlib.Analysis.Complex.RemovableSingularity
/-- **Removable singularity** theorem: if `s` is a neighborhood of `c : ℂ`, a function `f : ℂ → E`
is complex differentiable and is bounded on `s \ {c}`, then `f` redefined to be equal to
`limUnder (𝓝[≠] c) f` at `c` is complex differentiable on `s`.  -/
Complex.differentiableOn_update_limUnder_of_bddAbove : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {s : Set ℂ}
  {c : ℂ},
  s ∈ nhds c →
    DifferentiableOn ℂ f (s \ {c}) →
      BddAbove (norm ∘ f '' (s \ {c})) → DifferentiableOn ℂ (Function.update f c ((nhdsWithin c {c}ᶜ).limUnder f)) s
-- Mathlib.Combinatorics.SimpleGraph.Density
Rel.card_interedges_add_card_interedges_compl : ∀ {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [inst : (a : α) → DecidablePred (r a)] (s : Finset α) (t : Finset β),
  (Rel.interedges r s t).card + (Rel.interedges (fun x y => ¬r x y) s t).card = s.card * t.card
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.head_main_ok : ∀ {q : Turing.PartrecToTM2.Λ'} {s : Option Turing.PartrecToTM2.Γ'} {L : List ℕ} {c d : List Turing.PartrecToTM2.Γ'},
  StateTransition.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr)
    { l := some (Turing.PartrecToTM2.head Turing.PartrecToTM2.K'.main q), var := s,
      stk := Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList L) [] c d }
    { l := some q, var := none, stk := Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList [L.headI]) [] c d }
-- Batteries.Data.DList.Lemmas
_private.Batteries.Data.DList.Lemmas.0.Batteries.DList.toList.match_1.splitter : {α : Type u_1} →
  (motive : Batteries.DList α → Sort u_2) →
    (x : Batteries.DList α) →
      ((f : List α → List α) →
          (invariant : ∀ (l : List α), f l = f [] ++ l) → motive { apply := f, invariant := invariant }) →
        motive x
-- Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
HasEnoughRootsOfUnity.of_card_le : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {n : ℕ} [NeZero n],
  n ≤ Nat.card ↥(rootsOfUnity n R) → HasEnoughRootsOfUnity R n
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.monic_geom_sum_X : ∀ {R : Type u} [inst : Semiring R] {n : ℕ}, n ≠ 0 → (∑ i ∈ Finset.range n, Polynomial.X ^ i).Monic
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocIso_inv_naturality_assoc : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {d₁ d₂ : D} {c₁ c₂ c₃ c₄ : C} (f : d₁ ⟶ d₂)
  (g : c₁ ⟶ c₂) (h : c₃ ⟶ c₄) {Z : D}
  (h_1 :
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d₂
        (CategoryTheory.MonoidalCategoryStruct.tensorObj c₂ c₄) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f g) h)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d₂ c₂ c₄).inv h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d₁ c₁ c₃).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f
          (CategoryTheory.MonoidalCategoryStruct.tensorHom g h))
        h_1)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.ofLinearEquiv_apply : ∀ {k : Type u_10} {V : Type u_11} {P : Type u_12} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (A : V ≃ₗ[k] V) (p₀ p₁ x : P), (AffineEquiv.ofLinearEquiv A p₀ p₁) x = A (x -ᵥ p₀) +ᵥ p₁
-- Mathlib.GroupTheory.Congruence.Hom
AddCon.hom_ext_iff : ∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] {c : AddCon M}
  {f g : c.Quotient →+ P}, f = g ↔ f.comp c.mk' = g.comp c.mk'
-- Mathlib.CategoryTheory.CopyDiscardCategory.Basic
/-- Copy on the unit object.  -/
CategoryTheory.CopyDiscardCategory.copy_unit : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.CopyDiscardCategory C],
  CategoryTheory.ComonObj.comul =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
-- Mathlib.LinearAlgebra.Finsupp.Defs
Module.subsingletonEquiv_symm_apply : ∀ (R : Type u_4) (M : Type u_5) (ι : Type u_6) [inst : Semiring R] [inst_1 : Subsingleton R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (x : ι →₀ R), (Module.subsingletonEquiv R M ι).symm x = 0
-- Init.Data.UInt.Bitwise
UInt64.toNat_and : ∀ (a b : UInt64), (a &&& b).toNat = a.toNat &&& b.toNat
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
Ordinal.CNF.coeff_opow_mul_add : ∀ {b e x y : Ordinal.{u_1}},
  1 < b → x ≠ 0 → x < b → y < b ^ e → Ordinal.CNF.coeff b (b ^ e * x + y) = (fun₀ | e => x) + Ordinal.CNF.coeff b y
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.eval_part : Partrec₂ Nat.Partrec.Code.eval
-- Aesop.Tree.Data
Aesop.GoalState.unknown : Aesop.GoalState
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.registerSolverExtension.unsafe_impl_2 : {σ : Type} → Lean.Meta.Grind.SolverExtension σ → Lean.Meta.Grind.SolverExtension Lean.Meta.Grind.SolverExtensionState
-- Mathlib.CategoryTheory.Limits.MorphismProperty
CategoryTheory.MorphismProperty.Over.instHasFiniteLimitsTopOfHasFiniteWidePullbacks : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) (X : T)
  [CategoryTheory.Limits.HasPullbacks T] [P.IsMultiplicative] [P.IsStableUnderBaseChange] [P.HasOfPostcompProperty P]
  [CategoryTheory.Limits.HasFiniteWidePullbacks T], CategoryTheory.Limits.HasFiniteLimits (P.Over ⊤ X)
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.PartialFixpointType.noConfusionType : Sort v✝ → Lean.Elab.PartialFixpointType → Lean.Elab.PartialFixpointType → Sort v✝
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.direction.eq_1 : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s : AffineSubspace k P), s.direction = vectorSpan k ↑s
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.toArray.congr_simp : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.Rxc.IsAlwaysFinite α] (r r_1 : Std.Rcc α),
  r = r_1 → r.toArray = r_1.toArray
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.FinitaryExtensive.isVanKampen_finiteCoproducts_Fin : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryExtensive C] {n : ℕ}
  {F : CategoryTheory.Functor (CategoryTheory.Discrete (Fin n)) C} {c : CategoryTheory.Limits.Cocone F}
  (hc : CategoryTheory.Limits.IsColimit c), CategoryTheory.IsVanKampenColimit c
-- Mathlib.Topology.MetricSpace.Cover
/-- A set in a proper metric space which admits a compact cover is relatively compact.  -/
Metric.IsCover.isCompact_closure : ∀ {X : Type u_1} [inst : MetricSpace X] [ProperSpace X] {ε : NNReal} {s N : Set X},
  Metric.IsCover ε s N → IsCompact N → IsCompact (closure s)
-- Batteries.Data.BinomialHeap.Basic
/-- `O(1)`. Auxiliary for `Heap.merge`: Is the minimum rank in `Heap` strictly larger than `n`?  -/
Batteries.BinomialHeap.Imp.Heap.rankGT : {α : Type u_1} → Batteries.BinomialHeap.Imp.Heap α → ℕ → Prop
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
/-- Reinterpret a continuous linear equivalence between modules
as a continuous affine equivalence.  -/
ContinuousLinearEquiv.toContinuousAffineEquiv : {k : Type u_1} →
  [inst : Ring k] →
    {E : Type u_10} →
      {F : Type u_11} →
        [inst_1 : AddCommGroup E] →
          [inst_2 : Module k E] →
            [inst_3 : TopologicalSpace E] →
              [inst_4 : AddCommGroup F] →
                [inst_5 : Module k F] → [inst_6 : TopologicalSpace F] → (E ≃L[k] F) → E ≃ᴬ[k] F
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.of_eq : ∀ {M : Type u_1} [inst : Monoid M] {a b : M}, a = b → Associated a b
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.unitOfList_singleton : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {k : α},
  Std.ExtDHashMap.Const.unitOfList [k] = ∅.insertIfNew k ()
-- Batteries.Tactic.PrintDependents
/-- Constructs the initial state, marking the constants in `cs`. The result of `collect` will say
whether a given declaration depends transitively on one of these constants.

If `otherAxiom` is true, any axiom not specified in `cs` will also be tracked.
 -/
Batteries.Tactic.CollectDependents.mkState : Array (Lean.Name × Bool) → optParam Bool true → Batteries.Tactic.CollectDependents.State
-- Init.Data.Iterators.Basic
Std.IterStep.mapIterator_done : ∀ {α : Type u} {β : Type w} {α' : Type u'} {f : α → α'},
  Std.IterStep.mapIterator f Std.IterStep.done = Std.IterStep.done
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.GenPatternInfo.heq : Lean.Meta.Grind.GenPatternInfo → Bool
-- Init.Data.Array.Lemmas
Array.forall_mem_flatMap : ∀ {β : Type u_1} {α : Type u_2} {p : β → Prop} {xs : Array α} {f : α → Array β},
  (∀ x ∈ Array.flatMap f xs, p x) ↔ ∀ a ∈ xs, ∀ b ∈ f a, p b
-- Mathlib.Data.List.Forall2
List.Forall₂.length_eq : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {l₁ : List α} {l₂ : List β},
  List.Forall₂ R l₁ l₂ → l₁.length = l₂.length
-- Mathlib.NumberTheory.Real.Irrational
Irrational.of_ratCast_sub : ∀ (q : ℚ) {x : ℝ}, Irrational (↑q - x) → Irrational x
-- Init.LawfulBEqTactics
DerivingHelpers.and_true_curry : ∀ {a b : Bool} {P : Prop}, (a = true → b = true → P) → (a && b) = true → P
-- Init.Data.Float.Float32
/-- Computes the natural logarithm `ln x` of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`logf`.
 -/
Float32.log : Float32 → Float32
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
FundamentalGroupoid.conj_eqToHom : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y x' y' : X} {p : Path.Homotopic.Quotient x y} (hx : x' = x)
  (hy : y' = y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp p (CategoryTheory.eqToHom ⋯)) =
    p.cast hx hy
-- Init.Data.BitVec.Lemmas
BitVec.sub_add_cancel : ∀ {w : ℕ} (x y : BitVec w), x - y + y = x
-- Mathlib.Analysis.InnerProductSpace.Affine
inner_vsub_vsub_right_eq_dist_sq_right_iff : ∀ {V : Type u_2} {P : Type u_3} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {a b c : P}, inner ℝ (a -ᵥ c) (b -ᵥ c) = dist b c ^ 2 ↔ inner ℝ (a -ᵥ b) (b -ᵥ c) = 0
-- Init.Data.String.Bootstrap
Substring.Raw.Internal.toString : Substring.Raw → String
-- Mathlib.Topology.Constructions
nhds_pi : ∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] {a : (i : ι) → A i},
  nhds a = Filter.pi fun i => nhds (a i)
-- Lean.Widget.UserWidget
Lean.Widget.WidgetSource.mk : String → Lean.Widget.WidgetSource
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k fallback : α},
  k ∉ t₂ → (t₁ ∩ t₂).getKeyD k fallback = fallback
-- Mathlib.Analysis.InnerProductSpace.l2Space
IsHilbertSum.linearIsometryEquiv.congr_simp : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {G : ι → Type u_4} [inst_3 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] [inst_5 : CompleteSpace E] {V V_1 : (i : ι) → G i →ₗᵢ[𝕜] E}
  (e_V : V = V_1) (hV : IsHilbertSum 𝕜 G V), hV.linearIsometryEquiv = ⋯.linearIsometryEquiv
-- Init.Data.Array.Attach
Array.attach_filterMap : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Option β},
  (Array.filterMap f xs).attach =
    Array.filterMap
      (fun x =>
        match x with
        | ⟨x, h⟩ => (f x).pbind fun b m => some ⟨b, ⋯⟩)
      xs.attach
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.lift_comp_inr : ∀ {N : Type u_1} {G : Type u_2} {H : Type u_3} [inst : Group N] [inst_1 : Group G] [inst_2 : Group H]
  {φ : G →* MulAut N} (fn : N →* H) (fg : G →* H)
  (h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn),
  (SemidirectProduct.lift fn fg h).comp SemidirectProduct.inr = fg
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.popWhile.eq_def : ∀ {α : Type u} (p : α → Bool) (as : Array α),
  Array.popWhile p as = if h : as.size > 0 then if p as[as.size - 1] = true then Array.popWhile p as.pop else as else as
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
UniformContinuous.sub_const : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α]
  [inst_3 : UniformSpace β] {f : β → α}, UniformContinuous f → ∀ (a : α), UniformContinuous fun x => f x - a
-- Mathlib.Computability.TuringMachine.StackTuringMachine
/-- The effect of a stack action on the stack.  -/
Turing.TM2to1.stWrite : {K : Type u_1} →
  {Γ : K → Type u_2} → {σ : Type u_4} → {k : K} → σ → List (Γ k) → Turing.TM2to1.StAct K Γ σ k → List (Γ k)
-- Lean.MetavarContext
Lean.DelayedMetavarAssignment.mk : Array Lean.Expr → Lean.MVarId → Lean.DelayedMetavarAssignment
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.realize_graph : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {n : ℕ} {f : L.Functions n} {x : Fin n → M} {y : M},
  (FirstOrder.Language.Formula.graph f).Realize (Fin.cons y x) ↔ FirstOrder.Language.Structure.funMap f x = y
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
/-- The canonical continuous multilinear map from `E = Πᵢ Eᵢ` to `⨂[𝕜] i, Eᵢ`.  -/
PiTensorProduct.tprodL : {ι : Type u_1} →
  [inst : Fintype ι] →
    (𝕜 : Type u_2) →
      {E : ι → Type u_3} →
        [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] →
          [inst_2 : NontriviallyNormedField 𝕜] →
            [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] → ContinuousMultilinearMap 𝕜 E (PiTensorProduct 𝕜 fun i => E i)
-- Lean.Elab.App
Lean.Elab.Term.ElabElimInfo.mk.injEq : ∀ (elimExpr elimType : Lean.Expr) (motivePos : ℕ) (majorsPos : Array ℕ) (elimExpr_1 elimType_1 : Lean.Expr)
  (motivePos_1 : ℕ) (majorsPos_1 : Array ℕ),
  ({ elimExpr := elimExpr, elimType := elimType, motivePos := motivePos, majorsPos := majorsPos } =
      { elimExpr := elimExpr_1, elimType := elimType_1, motivePos := motivePos_1, majorsPos := majorsPos_1 }) =
    (elimExpr = elimExpr_1 ∧ elimType = elimType_1 ∧ motivePos = motivePos_1 ∧ majorsPos = majorsPos_1)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
ModularForm.E.congr_simp : ∀ {k : ℕ} (hk : 3 ≤ k), ModularForm.E hk = ModularForm.E hk
-- Mathlib.CategoryTheory.Monoidal.Braided.Transport
CategoryTheory.Monoidal.Transported.instBraidedCategory.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.BraidedCategory C],
  CategoryTheory.Monoidal.Transported.instBraidedCategory e =
    CategoryTheory.BraidedCategory.ofFaithful e.inverse
      (fun x x_1 => e.functor.mapIso (β_ (e.inverse.obj x) (e.inverse.obj x_1))) ⋯
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.contract_coloops_eq : ∀ {α : Type u_1} (M : Matroid α) (C : Set α), (M.contract C).coloops = M.coloops \ C
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getKeyLE?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.Equiv t₂ → t₁.getKeyLE? k = t₂.getKeyLE? k
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.ext : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : Monoid A]
  [inst_3 : MulDistribMulAction M A] {B : Type u_5} [inst_4 : Monoid B] [inst_5 : MulDistribMulAction N B]
  {f g : A →ₑ*[φ] B}, (∀ (x : A), f x = g x) → f = g
-- Lean.Data.Json.FromToJson.Basic
Lean.Array.fromJson? : {α : Type u_1} → [Lean.FromJson α] → Lean.Json → Except String (Array α)
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonCommand.toJson : Lean.Lsp.Command → Lean.Json
-- Mathlib.CategoryTheory.Yoneda
/-- Unification hint for `(uliftCoyoneda.{w}.obj (op X)).obj Y = ULift (Y ⟶ X)`.  -/
CategoryTheory.uliftCoyoneda_obj_obj_eq_hom : {C : Type u₁} → [CategoryTheory.Category.{v₁, u₁} C] → C → C → C → C → Prop
-- Init.System.IOError
IO.Error.hardwareFault.inj : ∀ {osCode : UInt32} {details : String} {osCode_1 : UInt32} {details_1 : String},
  IO.Error.hardwareFault osCode details = IO.Error.hardwareFault osCode_1 details_1 →
    osCode = osCode_1 ∧ details = details_1
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
/-- If `f : M → N` is an additive monoid hom, then `MonoidAlgebra.mapDomain f` is a bialgebra hom
between their additive monoid algebras.  -/
AddMonoidAlgebra.mapDomainBialgHom : (R : Type u_1) →
  {M : Type u_8} →
    {N : Type u_9} →
      [inst : CommSemiring R] →
        [inst_1 : AddMonoid M] → [inst_2 : AddMonoid N] → (M →+ N) → AddMonoidAlgebra R M →ₐc[R] AddMonoidAlgebra R N
-- Mathlib.Data.PFun
PFun.get_prodLift : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α →. β) (g : α →. γ) (x : α) (h : (f.prodLift g x).Dom),
  (f.prodLift g x).get h = ((f x).get ⋯, (g x).get ⋯)
-- Init.Data.Array.Zip
Array.map_snd_zip : ∀ {α : Type u_1} {β : Type u_2} {as : Array α} {bs : Array β}, bs.size ≤ as.size → Array.map Prod.snd (as.zip bs) = bs
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t₂ → (t₁ \ t₂)[k]? = none
-- Std.Time.Format
/-- Formats a `DateTime` value into an RFC822 format string.
 -/
Std.Time.DateTime.toRFC822String : Std.Time.DateTime → String
-- Init.Data.String.Lemmas.Pattern.Split.Char
String.Slice.Pattern.Model.split_char_eq_split_beq : ∀ {c : Char} {s : String.Slice} (f curr : s.Pos) (hle : f ≤ curr),
  String.Slice.Pattern.Model.split c f curr hle = String.Slice.Pattern.Model.split (fun x => x == c) f curr hle
-- Mathlib.Order.Disjoint
eq_bot_of_top_isCompl : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : BoundedOrder α] {x : α}, IsCompl ⊤ x → x = ⊥
-- Mathlib.Topology.Constructions
continuous_uliftMap : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
  Continuous f → Continuous (ULift.map f)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instAddMonoidWithOne : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → AddMonoidWithOne (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] → AddMonoidWithOne (DirectLimit G f)
-- Mathlib.Order.RelClasses
OrderDual.total_le : ∀ {α : Type u} [inst : LE α] [h : Std.Total fun x1 x2 => x1 ≤ x2], Std.Total fun x1 x2 => x1 ≤ x2
-- Mathlib.CategoryTheory.ObjectProperty.Shift
/-- `P : ObjectProperty C` is stable under the shift by `A` if
`P X` implies `P X⟦a⟧` for any `a : A`.  -/
CategoryTheory.ObjectProperty.IsStableUnderShift : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.ObjectProperty C → (A : Type u_2) → [inst_1 : AddMonoid A] → [CategoryTheory.HasShift C A] → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.hasCoproductsOfShape_of_hasCoproducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] (J : Type w),
  CategoryTheory.Limits.HasCoproductsOfShape J C
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.LeftExactFunctor.whiskeringRight_obj_obj_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : D ⥤ₗ E) (X : C ⥤ₗ D),
  (((CategoryTheory.LeftExactFunctor.whiskeringRight C D E).obj F).obj X).obj = X.obj.comp F.obj