mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.CompleteBooleanAlgebra
/-- Pullback an `Order.Frame` along an injection.  -/
Function.Injective.frame : {α : Type u} →
  {β : Type v} →
    [inst : Max α] →
      [inst_1 : Min α] →
        [inst_2 : LE α] →
          [inst_3 : LT α] →
            [inst_4 : SupSet α] →
              [inst_5 : InfSet α] →
                [inst_6 : Top α] →
                  [inst_7 : Bot α] →
                    [inst_8 : Compl α] →
                      [inst_9 : HImp α] →
                        [inst_10 : Order.Frame β] →
                          (f : α → β) →
                            Function.Injective f →
                              (∀ {x y : α}, f x ≤ f y ↔ x ≤ y) →
                                (∀ {x y : α}, f x < f y ↔ x < y) →
                                  (∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) →
                                    (∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) →
                                      (∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) →
                                        (∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) →
                                          f ⊤ = ⊤ →
                                            f ⊥ = ⊥ →
                                              (∀ (a : α), f aᶜ = (f a)ᶜ) →
                                                (∀ (a b : α), f (a ⇨ b) = f a ⇨ f b) → Order.Frame α
-- Lean.LibrarySuggestions.Basic
Lean.LibrarySuggestions.Suggestion.mk.inj : ∀ {name : Lean.Name} {score : Float} {flag : Option String} {name_1 : Lean.Name} {score_1 : Float}
  {flag_1 : Option String},
  { name := name, score := score, flag := flag } = { name := name_1, score := score_1, flag := flag_1 } →
    name = name_1 ∧ score = score_1 ∧ flag = flag_1
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.ordered_insertₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {k : α} {v : β k} {l : Std.DTreeMap.Internal.Impl α β}
  (hlb : l.Balanced), l.Ordered → (Std.DTreeMap.Internal.Impl.insertₘ k v l hlb).Ordered
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_list_equiv_congr : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => Unit},
  (↑m₁).WF →
    (↑m₂).WF →
      (↑m₁).Equiv ↑m₂ →
        ∀ {l : List α},
          (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m₁ l)).Equiv
            ↑↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m₂ l)
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.M.run' : {α : Type} → Lean.Meta.Grind.EMatch.M α → Lean.Meta.Grind.GoalM α
-- Mathlib.Data.Nat.Digits.Lemmas
Nat.dvd_ofDigits_sub_ofDigits : ∀ {α : Type u_1} [inst : CommRing α] {a b k : α}, k ∣ a - b → ∀ (L : List ℕ), k ∣ Nat.ofDigits a L - Nat.ofDigits b L
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.instT3Space : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞}, T3Space (TestFunction Ω F n)
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
eq_tsub_iff_add_eq_of_le : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α], c ≤ b → (a = b - c ↔ a + c = b)
-- Lean.Elab.PatternVar
/-- Return the pattern variables occurring in the given patterns.
This method is used in the `match` and `do` notation elaborators
 -/
Lean.Elab.Term.getPatternsVars : Array Lean.Syntax → Lean.Elab.TermElabM (Array Lean.Elab.Term.PatternVar)
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
/-- The object on position `pq` on the `r`th page of the spectral sequence identifies
to `E^{deg pq}(i₀ ≤ i₁ ≤ i₂ ≤ i₃)`.  -/
CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageXIso : {C : Type u_1} →
  {ι : Type u_2} →
    {κ : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Abelian C] →
          [inst_2 : Preorder ι] →
            (X : CategoryTheory.Abelian.SpectralObject C ι) →
              {c : ℤ → ComplexShape κ} →
                {r₀ : ℤ} →
                  (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) →
                    (r : ℤ) →
                      (hr : r₀ ≤ r) →
                        (pq : κ) →
                          (i₀ i₁ i₂ i₃ : ι) →
                            (h₀ : i₀ = data.i₀ r pq ⋯) →
                              (h₁ : i₁ = data.i₁ pq) →
                                (h₂ : i₂ = data.i₂ pq) →
                                  (h₃ : i₃ = data.i₃ r pq ⋯) →
                                    (n₀ n₁ n₂ : ℤ) →
                                      n₁ = data.deg pq →
                                        (hn₁ :
                                            autoParam (n₀ + 1 = n₁)
                                              CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageXIso._auto_1) →
                                          (hn₂ :
                                              autoParam (n₁ + 1 = n₂)
                                                CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageXIso._auto_3) →
                                            CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageX X data r pq
                                                hr ≅
                                              X.E (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯)
                                                (CategoryTheory.homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂
-- Mathlib.Analysis.Asymptotics.Defs
/-- Definition of `IsBigO` in terms of filters.  -/
Asymptotics.isBigO_iff : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F} {l : Filter α},
  f =O[l] g ↔ ∃ c, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
-- Std.Http.Data.Method
/-- Put a resource under version control.
Source: https://www.rfc-editor.org/rfc/rfc3253#section-3.5
 -/
Std.Http.Method.versionControl : Std.Http.Method
-- Mathlib.Tactic.ClickSuggestions.Rewrite
Mathlib.Tactic.ClickSuggestions.RwLemma.mk.sizeOf_spec : ∀ (name : Mathlib.Tactic.ClickSuggestions.Premise) (symm : Bool),
  sizeOf { name := name, symm := symm } = 1 + sizeOf name + sizeOf symm
-- Mathlib.Data.Finsupp.Option
Finsupp.optionElim_some : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (f : Option α →₀ M), Finsupp.optionElim (f none) f.some = f
-- Init.Data.Slice.List.Basic
/-- The relevant suffix of the underlying list.  -/
Std.Slice.Internal.ListSliceData.list : {α : Type u} → Std.Slice.Internal.ListSliceData α → List α
-- Mathlib.GroupTheory.Perm.Closure
Equiv.Perm.closure_cycle_adjacent_swap : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {σ : Equiv.Perm α},
  σ.IsCycle → σ.support = Finset.univ → ∀ (x : α), Subgroup.closure {σ, Equiv.swap x (σ x)} = ⊤
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitNatIso_inv_app : ∀ (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.MonoidalLeftAction C D] (X : D),
  (CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitNatIso C D).inv.app X =
    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).inv
-- Batteries.Data.Fin.Lemmas
Fin.map_rev_find? : ∀ {n : ℕ} {p : Fin n → Bool}, Option.map Fin.rev (Fin.find? fun x => p x.rev) = Fin.findRev? p
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.fullSubcategoryInclusion_additive : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (Z : CategoryTheory.ObjectProperty C), Z.ι.Additive
-- Mathlib.AlgebraicTopology.SimplicialSet.Boundary
SSet.stdSimplex.notMem_boundary : ∀ (n : ℕ), SSet.stdSimplex.objMk OrderHom.id ∉ (SSet.boundary n).obj (Opposite.op { len := n })
-- Lean.Parser.Basic
Lean.Parser.instInhabitedPrattParsingTables : Inhabited Lean.Parser.PrattParsingTables
-- Mathlib.Tactic.Positivity.Basic
/-- Extension for the `positivity` tactic: nonnegative maps take nonnegative values.  -/
Mathlib.Meta.Positivity.evalMap : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.transpose_mono : ∀ {μ ν : YoungDiagram}, μ ≤ ν → μ.transpose ≤ ν.transpose
-- Mathlib.Geometry.Manifold.Notation
/-- Information about a model with corners found through `findModelInner`.
It includes the model with corners found, and, if this model is the trivial model with corners on a
normed space, information about that normed space. (Knowing this is important for forming products
of models.)

Most search results are not a model with corners for a normed space, so an `Expr` representing the
model with corners may be coerced directly to this type.
 -/
Manifold.Elab.FindModelResult : Type
-- Mathlib.Tactic.DepRewrite
/-- A proof of `p = x`. Must be an fvar.  -/
Mathlib.Tactic.DepRewrite.Context.h : Mathlib.Tactic.DepRewrite.Context → Lean.Expr
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.eq_zero_of_isEmpty_left : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β)
  [h : IsEmpty α], κ = 0
-- Std.Data.DHashMap.Basic
Std.DHashMap.instEmptyCollection : {α : Type u} → {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → EmptyCollection (Std.DHashMap α β)
-- Mathlib.NumberTheory.Padics.AddChar
PadicInt.continuousAddCharEquiv_of_norm_mul_apply : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : NormedRing R] [inst_2 : Algebra ℤ_[p] R]
  [inst_3 : IsBoundedSMul ℤ_[p] R] [inst_4 : IsUltrametricDist R] [inst_5 : CompleteSpace R] [inst_6 : NormMulClass R]
  {κ : AddChar ℤ_[p] R} (hκ : Continuous ⇑κ), ↑((PadicInt.continuousAddCharEquiv_of_norm_mul p R) ⟨κ, hκ⟩) = κ 1 - 1
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LeftLinear.δₗ_comp_μₗ_assoc : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'} [self : F.LeftLinear C] (c : C) (d : D) {Z : D'}
  (h : F.obj (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxLeftLinear.δₗ F c d)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxLeftLinear.μₗ F c d) h) =
    h
-- Mathlib.RingTheory.Teichmuller
_private.Mathlib.RingTheory.Teichmuller.0.Perfection.teichmullerAux.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicofork.fst_app_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  {I : CategoryTheory.Limits.MultispanIndex J C} (K : CategoryTheory.Limits.Multicofork I) (a : J.L),
  K.ι.app (CategoryTheory.Limits.WalkingMultispan.left a) = CategoryTheory.CategoryStruct.comp (I.fst a) (K.π (J.fst a))
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_pair_sub_right : ∀ {α : Type u} [inst : Ring α] (x y : α), Ideal.span {x - y, y} = Ideal.span {x, y}
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.instModuleQuotientIdealSpanSingletonSetSubtypeMemTorsionBy : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → (a : R) → Module (R ⧸ Ideal.span {a}) ↥(Submodule.torsionBy R M a)
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.isoShift_inv_naturality : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : F.ShiftSequence M] (n : M) {X Y : C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((F.shift n).map f) ((F.isoShift n).inv.app Y) =
    CategoryTheory.CategoryStruct.comp ((F.isoShift n).inv.app X) (F.map ((CategoryTheory.shiftFunctor C n).map f))
-- Lean.Meta.NatInstTesters
Lean.Meta.DefEq.isInstHAddNat : Lean.Expr → Lean.MetaM Bool
-- Lean.Elab.ConfigEval.Commands
/-- - `key` matches a specific key
- `key.*` matches any keys for which `key` is a proper prefix
- `*` matches all keys
 -/
Lean.Elab.ConfigEval.configEntryHandlerKey : Lean.ParserDescr
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
/-- Injection of `X` in the optimal coupling between `X` and `Y`  -/
GromovHausdorff.optimalGHInjl : (X : Type u) →
  (Y : Type v) →
    [inst : MetricSpace X] →
      [inst_1 : CompactSpace X] →
        [inst_2 : Nonempty X] →
          [inst_3 : MetricSpace Y] →
            [inst_4 : CompactSpace Y] → [inst_5 : Nonempty Y] → X → GromovHausdorff.OptimalGHCoupling X Y
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedSubgroup.instSemilatticeInfClosedSubgroup.eq_1 : ∀ (G : Type u) [inst : Group G] [inst_1 : TopologicalSpace G],
  ClosedSubgroup.instSemilatticeInfClosedSubgroup G = Function.Injective.semilatticeInf SetLike.coe ⋯ ⋯ ⋯ ⋯
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
/-- The ideal `⟨X - x, Y - y(X)⟩` of `R[W]` for some `x` in `R` and `y(X)` in `R[X]`.  -/
WeierstrassCurve.Affine.CoordinateRing.XYIdeal : {R : Type r} → [inst : CommRing R] → (W' : WeierstrassCurve.Affine R) → R → Polynomial R → Ideal W'.CoordinateRing
-- Mathlib.Topology.Order.Lattice
ContinuousWithinAt.inf' : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] [inst_2 : Min L]
  [ContinuousInf L] {f g : X → L} {s : Set X} {x : X},
  ContinuousWithinAt f s x → ContinuousWithinAt g s x → ContinuousWithinAt (f ⊓ g) s x
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.coe_of : ∀ (R : Type u) [inst : CommRing R] (X : Type v) [inst_1 : Ring X] [inst_2 : Algebra R X], ↑(AlgCat.of R X) = X
-- Lean.Meta.Tactic.Induction
Lean.Meta.instInhabitedAltVarNames : Inhabited Lean.Meta.AltVarNames
-- Mathlib.Analysis.Normed.Module.WeakDual
/-- A set in `StrongDual 𝕜 E` is bounded iff its image in `WeakDual 𝕜 E` is bounded.  -/
WeakDual.isBounded_toWeakDual_preimage_iff_isBounded : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set (WeakDual 𝕜 E)},
  Bornology.IsBounded (⇑StrongDual.toWeakDual ⁻¹' s) ↔ Bornology.IsBounded s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey_le_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} (hc : k ∈ t), (compare (t.minKey ⋯) k).isLE = true
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_eq_default : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {a : α}, a ∉ t → t.getKey! a = default
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.reflexivePair_obj_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} (f g : A ⟶ B) (s : B ⟶ A)
  {sl : CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id B}
  {sr : CategoryTheory.CategoryStruct.comp s g = CategoryTheory.CategoryStruct.id B},
  (CategoryTheory.Limits.reflexivePair f g s sl sr).obj CategoryTheory.Limits.WalkingReflexivePair.zero = B
-- Lean.Parser.Types
Lean.Parser.InputContext.mk' : (inputString : String) →
  String →
    Lean.FileMap →
      (endPos : String.Pos.Raw) →
        autoParam (endPos ≤ inputString.rawEndPos) Lean.Parser.InputContext.endPos_valid._autoParam →
          Lean.Parser.InputContext
-- Init.Data.String.Lemmas.Pattern.Find.Pred
String.Slice.contains_bool_eq : ∀ {p : Char → Bool} {s : String.Slice}, s.contains p = s.copy.toList.any p
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Set.Finite.toFinset_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] [inst_1 : DecidableEq β] {s : Set α} {t : Set β} (hs : s.Finite)
  (ht : t.Finite) (hf : optParam (s • t).Finite ⋯), hf.toFinset = hs.toFinset • ht.toFinset
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.size_le_size_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  t.size ≤ (t.erase k).size + 1
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.State : Type
-- Mathlib.Order.Interval.Finset.Gaps
/-- The first coordinate of `F.intervalGapsWithin h a b i` is `a` if `i = 0`,
`y (i - 1)` otherwise.  -/
Finset.intervalGapsWithin.fst : {α : Type u_1} → [LinearOrder α] → (F : Finset (α × α)) → {k : ℕ} → F.card = k → α → Fin (k + 1) → α
-- Mathlib.Analysis.Normed.Operator.NormedSpace
/-- Composing on the left with a linear isometry gives a linear isometry between spaces of
continuous linear maps.  -/
LinearIsometry.postcomp : {𝕜 : Type u_1} →
  {𝕜₂ : Type u_3} →
    {𝕜₃ : Type u_4} →
      {E : Type u_5} →
        {F : Type u_6} →
          {G : Type u_8} →
            [inst : SeminormedAddCommGroup E] →
              [inst_1 : SeminormedAddCommGroup F] →
                [inst_2 : SeminormedAddCommGroup G] →
                  [inst_3 : NontriviallyNormedField 𝕜] →
                    [inst_4 : NontriviallyNormedField 𝕜₂] →
                      [inst_5 : NontriviallyNormedField 𝕜₃] →
                        [inst_6 : NormedSpace 𝕜 E] →
                          [inst_7 : NormedSpace 𝕜₂ F] →
                            [inst_8 : NormedSpace 𝕜₃ G] →
                              {σ₁₂ : 𝕜 →+* 𝕜₂} →
                                {σ₂₃ : 𝕜₂ →+* 𝕜₃} →
                                  {σ₁₃ : 𝕜 →+* 𝕜₃} →
                                    [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] →
                                      [inst_10 : RingHomIsometric σ₁₂] →
                                        [inst_11 : RingHomIsometric σ₁₃] →
                                          (F →ₛₗᵢ[σ₂₃] G) → (E →SL[σ₁₂] F) →ₛₗᵢ[σ₂₃] E →SL[σ₁₃] G
-- Mathlib.Algebra.Order.BigOperators.Ring.Finset
AbsoluteValue.map_prod : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : CommSemiring R] [Nontrivial R] [inst_2 : CommRing S]
  [inst_3 : LinearOrder S] [IsStrictOrderedRing S] (abv : AbsoluteValue R S) (f : ι → R) (s : Finset ι),
  abv (∏ i ∈ s, f i) = ∏ i ∈ s, abv (f i)
-- Mathlib.RingTheory.LinearDisjoint
/-- Linear disjointness is preserved by injective algebra homomorphisms.  -/
Subalgebra.LinearDisjoint.map : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {A B : Subalgebra R S},
  A.LinearDisjoint B →
    ∀ {T : Type w} [inst_3 : Semiring T] [inst_4 : Algebra R T] (f : S →ₐ[R] T),
      Function.Injective ⇑f → (Subalgebra.map f A).LinearDisjoint (Subalgebra.map f B)
-- Mathlib.Tactic.Translate.UnfoldBoundary
_private.Mathlib.Tactic.Translate.UnfoldBoundary.0.Mathlib.Tactic.UnfoldBoundary.refoldConsts.go : Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries → Lean.Expr → Lean.MVarId → Lean.Meta.SimpM Unit
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
/-- The morphisms between the `obj` fields of descent data.  -/
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.Hom.hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F :
        CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
          (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)} →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} → {D₁ D₂ : F.DescentDataAsCoalgebra f} → D₁.Hom D₂ → (i : ι) → D₁.obj i ⟶ D₂.obj i
-- Mathlib.Data.Finset.Grade
CovBy.exists_multiset_cons : ∀ {α : Type u_1} {s t : Multiset α}, s ⋖ t → ∃ a, a ::ₘ s = t
-- Init.Data.Slice.Array.Iterator
_private.Init.Data.Slice.Array.Iterator.0.SubarrayIterator.step.match_1.eq_1 : ∀ {α : Type u_1} (motive : Std.IterM Id α → Sort u_2) (xs : Subarray α)
  (h_1 : (xs : Subarray α) → motive { internalState := { xs := xs } }),
  (match { internalState := { xs := xs } } with
    | { internalState := { xs := xs } } => h_1 xs) =
    h_1 xs
-- Mathlib.Topology.Irreducible
Set.Subsingleton.isPreirreducible : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, s.Subsingleton → IsPreirreducible s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Real.tan_eq_one_sub_tan_half_sq_div_one_add_tan_half_sq : ∀ (x : ℝ), Real.tan x = 2 * Real.tan (x / 2) / (1 - Real.tan (x / 2) ^ 2)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.denoteAsIntModule.go.eq_def : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) (m : Lean.Grind.CommRing.Mon)
  (acc : α),
  Lean.Grind.CommRing.Mon.denoteAsIntModule.go ctx m acc =
    match m with
    | Lean.Grind.CommRing.Mon.unit => acc
    | Lean.Grind.CommRing.Mon.mult pw m =>
      Lean.Grind.CommRing.Mon.denoteAsIntModule.go ctx m (acc * Lean.Grind.CommRing.Power.denote ctx pw)
-- Mathlib.Algebra.Order.Field.Basic
add_sub_div_two_lt : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α},
  a < b → a + (b - a) / 2 < b
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.mem_smul_set_iff_inv_smul_mem : ∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] {A : Set β} {a : α} {x : β},
  x ∈ a • A ↔ a⁻¹ • x ∈ A
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.radical_eq_one_iff : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a : M}, UniqueFactorizationMonoid.radical a = 1 ↔ a = 0 ∨ IsUnit a
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.brange_bfamilyOfFamily : ∀ {α : Type u_1} {ι : Type u} (f : ι → α),
  (Ordinal.type WellOrderingRel).brange (Ordinal.bfamilyOfFamily f) = Set.range f
-- Init.Data.BitVec.Lemmas
BitVec.signExtend_and : ∀ {w v : ℕ} {x y : BitVec w}, BitVec.signExtend v (x &&& y) = BitVec.signExtend v x &&& BitVec.signExtend v y
-- Lean.Meta.Tactic.Injection
Lean.Meta.InjectionResult.subgoal.sizeOf_spec : ∀ (mvarId : Lean.MVarId) (newEqs : Array Lean.FVarId) (remainingNames : List Lean.Name),
  sizeOf (Lean.Meta.InjectionResult.subgoal mvarId newEqs remainingNames) =
    1 + sizeOf mvarId + sizeOf newEqs + sizeOf remainingNames
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.IsAdjMatrix.compl_compl : ∀ {α : Type u_1} {V : Type u_2} [inst : DecidableEq α] [inst_1 : DecidableEq V] [inst_2 : Zero α] [inst_3 : One α]
  {A : Matrix V V α}, A.IsAdjMatrix → A.compl.compl = A
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.map_smulₑ : ∀ {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 : A →ₑ*[φ] B) (m : M) (x : A), f (m • x) = φ m • f x
-- Mathlib.Topology.Algebra.FilterBasis
GroupFilterBasis.nhds_eq : ∀ {G : Type u} [inst : Group G] (B : GroupFilterBasis G) {x₀ : G}, nhds x₀ = B.N x₀
-- Mathlib.Algebra.DirectSum.Algebra
/-- The piecewise multiplication from the `Mul` instance, as a bundled linear map.

This is the graded version of `LinearMap.mul`, and the linear version of `DirectSum.gMulHom`  -/
DirectSum.gMulLHom : {ι : Type uι} →
  (R : Type uR) →
    (A : ι → Type uA) →
      [inst : CommSemiring R] →
        [inst_1 : (i : ι) → AddCommMonoid (A i)] →
          [inst_2 : (i : ι) → Module R (A i)] →
            [inst_3 : AddMonoid ι] →
              [inst_4 : DirectSum.GSemiring A] → [DirectSum.GAlgebra R A] → {i j : ι} → A i →ₗ[R] A j →ₗ[R] A (i + j)
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.simprocExtensionMapRef : IO.Ref Lean.Meta.Simp.SimprocExtensionMap
-- Std.Tactic.BVDecide.LRAT.Parser
/-- Parse `proof` as an LRAT proof. `proof` may contain either the binary or the non-binary LRAT format.
 -/
Std.Tactic.BVDecide.LRAT.parseLRATProof : ByteArray → Except String (Array Std.Tactic.BVDecide.LRAT.IntAction)