mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.Transvection
/-- A transvection matrix is obtained from the identity by adding `c` times the `j`-th row to
the `i`-th row.  -/
Matrix.updateRow_eq_transvection : ∀ {n : Type u_1} {R : Type u₂} [inst : DecidableEq n] [inst_1 : CommRing R] (i j : n) [Finite n] (c : R),
  Matrix.updateRow 1 i (1 i + c • 1 j) = Matrix.transvection i j c
-- Mathlib.Data.Int.Fib.Basic
_private.Mathlib.Data.Int.Fib.Basic.0.Int.fib_add_natCast : ∀ (m : ℤ) (n : ℕ), Int.fib (m + ↑n) = Int.fib (m - 1) * Int.fib ↑n + Int.fib m * Int.fib (↑n + 1)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rcc_add_succ_right_eq_push : ∀ {m n : ℕ}, (m...=m + n + 1).toArray = (m...=m + n).toArray.push (m + n + 1)
-- Mathlib.Analysis.Normed.Operator.Mul
ContinuousLinearMap.opENorm_lsmul_le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {R : Type u_3} [inst_3 : SeminormedRing R] [inst_4 : NormedAlgebra 𝕜 R]
  [inst_5 : Module R E] [inst_6 : IsBoundedSMul R E] [inst_7 : IsScalarTower 𝕜 R E],
  ‖ContinuousLinearMap.lsmul 𝕜 R‖ₑ ≤ 1
-- Init.Data.Option.Monadic
Option.bindM_join : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Pure m] {f : α → m (Option β)}
  {o : Option (Option α)}, Option.bindM f o.join = Option.bindM (fun x => Option.bindM f x) o
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
/-- `TensorProduct.lid` preserves tensor products of quadratic forms.  -/
QuadraticForm.tensorLId : {R : Type uR} →
  {M₂ : Type uM₂} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M₂] →
        [inst_2 : Module R M₂] →
          [inst_3 : Invertible 2] →
            (Q₂ : QuadraticForm R M₂) → QuadraticMap.IsometryEquiv (QuadraticForm.tmul QuadraticMap.sq Q₂) Q₂
-- Lean.Data.Lsp.Internal
/-- Name of the declaration.  -/
Lean.Lsp.LeanDeclIdent.decl : Lean.Lsp.LeanDeclIdent → Lean.Name
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.RatCoeff.mk.sizeOf_spec : ∀ {u : Lean.Level} {α : Q(Type u)} {e : Q(«$α»)} (value : ℚ) (hyp : Option Lean.Expr),
  sizeOf { value := value, hyp := hyp } = 1 + sizeOf value + sizeOf hyp
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.brange_bfamilyOfFamily' : ∀ {α : Type u_1} {ι : Type u} (r : ι → ι → Prop) [inst : IsWellOrder ι r] (f : ι → α),
  (Ordinal.type r).brange (Ordinal.bfamilyOfFamily' r f) = Set.range f
-- Mathlib.Algebra.GradedMonoid
SetLike.GradedMonoid.toGradedMul : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {inst : SetLike S R} {inst_1 : Monoid R} {inst_2 : AddMonoid ι}
  {A : ι → S} [self : SetLike.GradedMonoid A], SetLike.GradedMul A
-- Mathlib.Data.Fin.Parity
Fin.even_of_odd : ∀ {n : ℕ}, Odd n → ∀ (k : Fin n), Even k
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonCompletionItem : Lean.FromJson Lean.Lsp.CompletionItem
-- Mathlib.RingTheory.MvPolynomial.Basic
MvPolynomial.restrictSupport_add : ∀ {σ : Type u} (R : Type v) [inst : CommSemiring R] (s t : Set (σ →₀ ℕ)),
  MvPolynomial.restrictSupport R (s + t) = MvPolynomial.restrictSupport R s * MvPolynomial.restrictSupport R t
-- Init.Data.Int.Linear
Int.Internal.Linear.not_le_norm_expr_cert.eq_1 : ∀ (lhs rhs : Int.Internal.Linear.Expr) (p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.not_le_norm_expr_cert lhs rhs p = p.beq' (((lhs.sub rhs).norm.mul_k (-1)).addConst_k 1)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toList_roc_eq_some : ∀ {m n : ℤ} {i : ℕ}, i < (n - m).toNat → (m<...=n).toList[i]? = some (m + 1 + ↑i)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.HasAdditiveReduction.toIsMinimal : ∀ {R : Type u_1} {inst : CommRing R} {inst_1 : IsDomain R} {inst_2 : IsDiscreteValuationRing R} {K : Type u_2}
  {inst_3 : Field K} {inst_4 : Algebra R K} {inst_5 : IsFractionRing R K} {W : WeierstrassCurve K}
  [self : WeierstrassCurve.HasAdditiveReduction R W], WeierstrassCurve.IsMinimal R W
-- Mathlib.Data.FunLike.Equiv
/-- The coercions are left inverses.  -/
EquivLike.left_inv : ∀ {E : Sort u_1} {α : outParam (Sort u_2)} {β : outParam (Sort u_3)} [self : EquivLike E α β] (e : E),
  Function.LeftInverse (EquivLike.inv e) (EquivLike.coe e)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_natTransTruncLTOfLE_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) (X : C) {Z : C}
  (h_1 : (CategoryTheory.shiftFunctor C 1).obj ((t.truncLT b).obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.truncGEδLT a).app X)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map ((t.natTransTruncLTOfLE a b h).app X))
        h_1) =
    CategoryTheory.CategoryStruct.comp ((t.natTransTruncGEOfLE a b h).app X)
      (CategoryTheory.CategoryStruct.comp ((t.truncGEδLT b).app X) h_1)
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.Lan.CommuteWith.of_lan_comp_iso : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  [inst_1 : CategoryTheory.Bicategory.HasLeftKanExtension f g] {x : B} {h : c ⟶ x}
  [inst_2 : CategoryTheory.Bicategory.HasLeftKanExtension f (CategoryTheory.CategoryStruct.comp g h)]
  (i :
    CategoryTheory.Bicategory.lan f (CategoryTheory.CategoryStruct.comp g h) ≅
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.lan f g) h),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.lanUnit f (CategoryTheory.CategoryStruct.comp g h))
        (CategoryTheory.Bicategory.whiskerLeft f i.hom) =
      CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.lanUnit f g) h)
        (CategoryTheory.Bicategory.associator f (CategoryTheory.Bicategory.lan f g) h).hom →
    CategoryTheory.Bicategory.Lan.CommuteWith f g h
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_ofList_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v : β} [inst_1 : Inhabited β],
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l → (k, v) ∈ l → (Std.ExtTreeMap.ofList l cmp)[k']! = v
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_of_mem_keys : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α}, k ∈ m.keys → k ∈ m
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.toList_rci : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] (t : Std.DTreeMap.Internal.Impl α fun x => β),
  t.Ordered →
    ∀ (lowerBound : α),
      Std.Slice.toList (Std.Rci.Sliceable.mkSlice t lowerBound...*) =
        List.filter (fun e => (compare e.1 lowerBound).isGE) (Std.DTreeMap.Internal.Impl.Const.toList t)
-- Mathlib.Computability.TuringMachine.Config
List.headI.eq_2 : ∀ {α : Type u_1} [inst : Inhabited α] (a : α) (tail : List α), (a :: tail).headI = a
-- Init.Data.BitVec.Lemmas
BitVec.ofInt_toInt : ∀ {w : ℕ} {x : BitVec w}, BitVec.ofInt w x.toInt = x
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.stieltjesOfMeasurableRat_eq : ∀ {α : Type u_1} {f : α → ℚ → ℝ} [inst : MeasurableSpace α] (hf : Measurable f) (a : α) (r : ℚ),
  ↑(ProbabilityTheory.stieltjesOfMeasurableRat f hf a) ↑r = ProbabilityTheory.toRatCDF f a r
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciInf_le_of_le' : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrderBot α] {f : ι → α} {a : α} (c : ι),
  f c ≤ a → iInf f ≤ a
-- Mathlib.Order.Bounds.Basic
upperBounds_singleton : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, upperBounds {a} = Set.Ici a
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!.congr_simp : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] (m m_1 : Std.DHashMap α β),
  m = m_1 → ∀ (a : α) [inst_1 : Inhabited (β a)], m.get! a = m_1.get! a
-- Lean.DocString.DeferredCheck
Lean.Doc.DeferredCheck.mk.inj : ∀ {site : Lean.Doc.DeferredCheckSite} {index : ℕ} {sourceString : String} {imports : Array Lean.Name}
  {currNamespace : Lean.Name} {openDecls : List Lean.OpenDecl} {options : Lean.Options} {check : Dynamic}
  {site_1 : Lean.Doc.DeferredCheckSite} {index_1 : ℕ} {sourceString_1 : String} {imports_1 : Array Lean.Name}
  {currNamespace_1 : Lean.Name} {openDecls_1 : List Lean.OpenDecl} {options_1 : Lean.Options} {check_1 : Dynamic},
  { site := site, index := index, sourceString := sourceString, imports := imports, currNamespace := currNamespace,
        openDecls := openDecls, options := options, check := check } =
      { site := site_1, index := index_1, sourceString := sourceString_1, imports := imports_1,
        currNamespace := currNamespace_1, openDecls := openDecls_1, options := options_1, check := check_1 } →
    site = site_1 ∧
      index = index_1 ∧
        sourceString = sourceString_1 ∧
          imports = imports_1 ∧
            currNamespace = currNamespace_1 ∧ openDecls = openDecls_1 ∧ options = options_1 ∧ check = check_1
-- Lean.DocString.Types
Lean.Doc.Part.brecOn_2.go : {i : Type u} →
  {b : Type v} →
    {p : Type w} →
      {motive_1 : Lean.Doc.Part i b p → Sort u_1} →
        {motive_2 : Array (Lean.Doc.Part i b p) → Sort u_1} →
          {motive_3 : List (Lean.Doc.Part i b p) → Sort u_1} →
            (t : List (Lean.Doc.Part i b p)) →
              ((t : Lean.Doc.Part i b p) → t.below → motive_1 t) →
                ((t : Array (Lean.Doc.Part i b p)) → Lean.Doc.Part.below_1 t → motive_2 t) →
                  ((t : List (Lean.Doc.Part i b p)) → Lean.Doc.Part.below_2 t → motive_3 t) →
                    motive_3 t ×' Lean.Doc.Part.below_2 t
-- Mathlib.Combinatorics.SetFamily.Compression.Down
/-- Image of the elements of `𝒜` which contain `a` under removing `a`. Finsets that do not contain
`a` such that `insert a s ∈ 𝒜`.  -/
Finset.memberSubfamily : {α : Type u_1} → [DecidableEq α] → α → Finset (Finset α) → Finset (Finset α)
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.lmapDomain_comp : ∀ {α : Type u_1} (M : Type u_2) (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {α' : Type u_9} {α'' : Type u_10} (f : α → α') (g : α' → α''),
  Finsupp.lmapDomain M R (g ∘ f) = Finsupp.lmapDomain M R g ∘ₗ Finsupp.lmapDomain M R f
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
/-- The infimum of `insert a s` is the minimum of `a` and the infimum of `s`, if `s` is
nonempty and bounded below.  -/
csInf_insert : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α},
  BddBelow s → s.Nonempty → sInf (insert a s) = a ⊓ sInf s
-- Mathlib.Algebra.Lie.Semisimple.Defs
LieAlgebra.IsSemisimple.mk : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  sSup {I | IsAtom I} = ⊤ →
    sSupIndep {I | IsAtom I} → (∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian ↥I) → LieAlgebra.IsSemisimple R L
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
/-- If `G` is a finite Galois group for `L/K`, `N` is a normal subgroup that is a Galois group for
`L/F`, and `H` is a subgroup that is a Galois group for `L/E` with `E ≤ F`, then the image of `H`
under the canonical quotient map `G → G ⧸ N` is a Galois group for `F/E`.  -/
IsGaloisGroup.map_quotientMk' : ∀ (G : Type u_1) (K : Type u_3) (L : Type u_4) [inst : Group G] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] (H : Subgroup G) (F : IntermediateField K L) (N : Subgroup G)
  [inst_5 : N.Normal] [inst_6 : IsGaloisGroup (↥N) (↥F) L] (E : IntermediateField K L) [hE : IsGaloisGroup (↥H) (↥E) L]
  [Finite G] [IsGaloisGroup G K L] (h : E ≤ F), IsGaloisGroup ↥(Subgroup.map (QuotientGroup.mk' N) H) ↥E ↥F
-- Mathlib.RingTheory.Valuation.Basic
Valuation.ext : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] {v₁ v₂ : Valuation R Γ₀},
  (∀ (r : R), v₁ r = v₂ r) → v₁ = v₂
-- Mathlib.Algebra.Group.Hom.Basic
ZeroHom.add_comp : ∀ {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : Zero M] [inst_1 : Zero N] [inst_2 : AddZeroClass P]
  (g₁ g₂ : ZeroHom N P) (f : ZeroHom M N), (g₁ + g₂).comp f = g₁.comp f + g₂.comp f
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
MeasureTheory.Measure.IicSnd_mono : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) {r r' : ℝ},
  r ≤ r' → ρ.IicSnd r ≤ ρ.IicSnd r'
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.instIsCardinalFilteredWithTopCarrierObjPartOrdEmbIsCardinalFiltered : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] (J : CategoryTheory.CardinalDirectedPoset κ) (κ' : Cardinal.{u})
  [inst_1 : Fact κ'.IsRegular], CategoryTheory.IsCardinalFiltered (WithTop ↑J.obj) κ'
-- Lean.Meta.Tactic.Grind.Main
_private.Lean.Meta.Tactic.Grind.Main.0.Lean.Meta.Grind.resolveDelayedMVarAssignments.go : Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Grind.AC
Lean.Grind.AC.Seq.concat_k_eq_concat : ∀ (s₁ s₂ : Lean.Grind.AC.Seq), s₁.concat_k s₂ = s₁.concat s₂
-- Mathlib.ModelTheory.Arithmetic.Presburger.Definability
FirstOrder.Language.Formula.iInf.congr_simp : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} [inst : Finite α] (f f_1 : α → L.Formula β),
  f = f_1 → FirstOrder.Language.Formula.iInf f = FirstOrder.Language.Formula.iInf f_1
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.homOfLE_ι : ∀ {X : SSet} {S₁ S₂ : X.Subcomplex} (h : S₁ ≤ S₂),
  CategoryTheory.CategoryStruct.comp (SSet.Subcomplex.homOfLE h) S₂.ι = S₁.ι
-- Mathlib.CategoryTheory.Category.ULift
CategoryTheory.AsSmall.up_map_down : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.AsSmall.up.map f).down = f
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
_private.Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme.0.AlgebraicGeometry.Scheme.IdealSheafData.glueDataT_fst : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U V : ↑X.affineOpens),
  CategoryTheory.CategoryStruct.comp (I.glueDataT U V)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯))
        (I.glueDataObjι V)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯))
      (X.homOfLE ⋯)
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.instCompleteLatticeHomClass : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice α] [inst_1 : CompleteLattice β],
  CompleteLatticeHomClass (CompleteLatticeHom α β) α β
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.instQuasiIsoNatToNormalizedChainComplex : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C) [inst_3 : CategoryTheory.CategoryWithHomology C],
  QuasiIso (X.toNormalizedChainComplex R)
-- Std.Data.Iterators.Lemmas.Producers.Vector
Vector.toList_iterFromIdx : ∀ {β : Type w} {n : ℕ} {xs : Vector β n} {pos : ℕ}, (xs.iterFromIdx pos).toList = List.drop pos xs.toList
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normalCore_eq_iInf_map_addConj : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.normalCore = ⨅ g, AddSubgroup.map (↑(AddAut.addConj g)) H
-- Mathlib.CategoryTheory.Sites.Monoidal
CategoryTheory.GrothendieckTopology.W.monoidal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₃}
  [inst_1 : CategoryTheory.Category.{v₃, u₃} A] [inst_2 : CategoryTheory.MonoidalCategory A]
  [inst_3 : CategoryTheory.MonoidalClosed A]
  [∀ (F₁ F₂ : CategoryTheory.Functor Cᵒᵖ A), CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom A F₁ F₂]
  [∀ (F₁ F₂ : CategoryTheory.Functor Cᵒᵖ A), CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom A F₁ F₂]
  [CategoryTheory.BraidedCategory A], J.W.IsMonoidal
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.add_left_cancel' : ∀ {n a b : ℕ} (c : ℕ), c + a ≡ c + b [MOD n] → a ≡ b [MOD n]
-- Mathlib.Data.PEquiv
PEquiv.symm_symm : ∀ {α : Type u} {β : Type v} (f : α ≃. β), f.symm.symm = f
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.ext_iff : ∀ {X : Type u_1} {R : Type u_2} {inst : Zero R} {inst_1 : Add R} {inst_2 : LE R} {x y : PseudoMetric X R},
  x = y ↔ x.toFun = y.toFun
-- Mathlib.RingTheory.PowerSeries.Order
/-- The order of the formal power series `1` is `0`.  -/
PowerSeries.order_one : ∀ {R : Type u_1} [inst : Semiring R] [Nontrivial R], PowerSeries.order 1 = 0
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- Construct an isomorphism of group objects by giving a monoid isomorphism between the underlying
objects.  -/
CategoryTheory.Grp.mkIso' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {G H : C} →
        (e : G ≅ H) →
          [inst_2 : CategoryTheory.GrpObj G] →
            [inst_3 : CategoryTheory.GrpObj H] →
              [CategoryTheory.IsMonHom e.hom] → { X := G, grp := inst_2 } ≅ { X := H, grp := inst_3 }
-- Mathlib.FieldTheory.Differential.Liouville
/-- We lift `isLiouville_of_finiteDimensional_galois` to non-Galois field extensions by using it for the
normal closure then obtaining it for `F`.
 -/
isLiouville_of_finiteDimensional : ∀ {F : Type u_1} {K : Type u_2} [inst : Field F] [inst_1 : Field K] [inst_2 : Differential F] [inst_3 : Differential K]
  [inst_4 : Algebra F K] [DifferentialAlgebra F K] [CharZero F] [FiniteDimensional F K], IsLiouville F K
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.skeletonEquivalence_functor : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C],
  (CategoryTheory.skeletonEquivalence C).functor = CategoryTheory.fromSkeleton C
-- Mathlib.CategoryTheory.Products.Associator
CategoryTheory.prod.associatorIsEquivalence : ∀ (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], (CategoryTheory.prod.associator C D E).IsEquivalence
-- Mathlib.Topology.Gluing
/-- An equivalence relation on `Σ i, D.U i` that holds iff `𝖣.ι i x = 𝖣.ι j y`.
See `TopCat.GlueData.ι_eq_iff_rel`.
 -/
TopCat.GlueData.Rel : (D : TopCat.GlueData) → (i : D.J) × ↑(D.U i) → (i : D.J) × ↑(D.U i) → Prop
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toSpanSingleton_apply_one : ∀ (R₁ : Type u_1) [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] [inst_4 : TopologicalSpace R₁] [inst_5 : ContinuousSMul R₁ M₁] (x : M₁),
  (ContinuousLinearMap.toSpanSingleton R₁ x) 1 = x
-- Mathlib.Topology.Algebra.FilterBasis
/-- If a module is endowed with a topological structure coming from
a module filter basis then it's a topological module.  -/
ModuleFilterBasis.continuousSMul : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : TopologicalSpace R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] (B : ModuleFilterBasis R M) [IsTopologicalRing R], ContinuousSMul R M
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
/-- the pushout cocone is a colimit  -/
CategoryTheory.IsPushout.isColimit' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P} (self : CategoryTheory.IsPushout f g inl inr),
  Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk inl inr ⋯))
-- Mathlib.CategoryTheory.GuitartExact.Opposite
CategoryTheory.TwoSquare.guitartExact_op_iff : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B),
  w.op.GuitartExact ↔ w.GuitartExact
-- Mathlib.Tactic.NormNum.Eq
Mathlib.Meta.NormNum.isRat_eq_false : ∀ {α : Type u_1} [inst : Ring α] [CharZero α] {a b : α} {na nb : ℤ} {da db : ℕ},
  Mathlib.Meta.NormNum.IsRat a na da →
    Mathlib.Meta.NormNum.IsRat b nb db → decide (na.mul (Int.ofNat db) = nb.mul (Int.ofNat da)) = false → ¬a = b
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roc_eq_toList_roo : ∀ {m n : ℕ}, (m<...=n).toList = (m<...n + 1).toList
-- Mathlib.RingTheory.WittVector.IsPoly
WittVector.IsPoly.mk' : ∀ {p : ℕ} {f : ⦃R : Type u_2⦄ → [CommRing R] → WittVector p R → WittVector p R},
  (∃ φ,
      ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : WittVector p R),
        (f x).coeff = fun n => (MvPolynomial.aeval x.coeff) (φ n)) →
    WittVector.IsPoly p f
-- Mathlib.Algebra.Category.Grp.Biproducts
AddCommGrpCat.instHasBinaryBiproducts : CategoryTheory.Limits.HasBinaryBiproducts AddCommGrpCat
-- Mathlib.MeasureTheory.Function.Piecewise
IndexedPartition.aemeasurable_piecewise : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] {s : ι → Set α} {f : ι → α → β}
  {μ : MeasureTheory.Measure α} [inst_1 : MeasurableSpace β] [Countable ι] (hs : IndexedPartition s),
  (∀ (i : ι), MeasurableSet (s i)) → (∀ (i : ι), AEMeasurable (f i) μ) → AEMeasurable (hs.piecewise f) μ
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.mem_of_mem_equivPair_tail : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → DecidableEq (M i)] {i j : ι} {w : Monoid.CoprodI.Word M} (m : M i),
  ⟨i, m⟩ ∈ ((Monoid.CoprodI.Word.equivPair j) w).tail.toList → ⟨i, m⟩ ∈ w.toList
-- Init.Data.Option.Lemmas
Option.max_eq_right_of_lt : ∀ {α : Type u_1} [inst : LT α] [inst_1 : Max α],
  (∀ (x y : α), y < x → x ⊔ y = x) → ∀ {a b : Option α}, b < a → a ⊔ b = a
-- Mathlib.RingTheory.Ideal.Over
Ideal.under_liesOver_of_liesOver : ∀ {A : Type u_2} [inst : CommSemiring A] (B : Type u_3) [inst_1 : CommSemiring B] {C : Type u_4} [inst_2 : Semiring C]
  [inst_3 : Algebra A B] [inst_4 : Algebra B C] [inst_5 : Algebra A C] [IsScalarTower A B C] (𝔓 : Ideal C) (p : Ideal A)
  [𝔓.LiesOver p], (Ideal.under B 𝔓).LiesOver p
-- Mathlib.Data.ENat.Basic
ENat.natCast_inj : ∀ {a b : ℕ}, ↑a = ↑b ↔ a = b
-- Mathlib.CategoryTheory.Whiskering
/-- Left-composition gives a functor `(C ⥤ D) ⥤ ((D ⥤ E) ⥤ (C ⥤ E))`.

`(whiskeringLeft.obj F).obj G` is `F ⋙ G`, and
`(whiskeringLeft.obj F).map α` is `whiskerLeft F α`.
 -/
CategoryTheory.Functor.whiskeringLeft : (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] →
            CategoryTheory.Functor (CategoryTheory.Functor C D)
              (CategoryTheory.Functor (CategoryTheory.Functor D E) (CategoryTheory.Functor C E))
-- Mathlib.Order.Filter.Extr
IsMaxFilter.min : ∀ {α : Type u} {β : Type v} [inst : LinearOrder β] {f g : α → β} {a : α} {l : Filter α},
  IsMaxFilter f l a → IsMaxFilter g l a → IsMaxFilter (fun x => min (f x) (g x)) l a
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.ae_eq_trim_of_stronglyMeasurable : ∀ {α : Type u_1} {E : Type u_5} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → E}
  [inst : TopologicalSpace E] [TopologicalSpace.MetrizableSpace E] (hm : m ≤ m₀),
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable g → f =ᵐ[μ] g → f =ᵐ[μ.trim hm] g
-- Init.Data.Bool
Bool.cond_eq_ite_iff : ∀ {α : Sort u_1} {a : Bool} {p : Prop} [h : Decidable p] {x y u v : α},
  ((bif a then x else y) = if p then u else v) ↔ (if a = true then x else y) = if p then u else v
-- Lean.Meta.LazyDiscrTree
/-- Index identifying trie in a discrimination tree.
 -/
Lean.Meta.LazyDiscrTree.TrieIndex : Type