mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.core.inj : ∀ {a b : Lean.Expr} {p₁ p₂ : Int.Internal.Linear.Poly} {a_1 b_1 : Lean.Expr} {p₁_1 p₂_1 : Int.Internal.Linear.Poly},
  Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.core a b p₁ p₂ =
      Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.core a_1 b_1 p₁_1 p₂_1 →
    a = a_1 ∧ b = b_1 ∧ p₁ = p₁_1 ∧ p₂ = p₂_1
-- Mathlib.Algebra.Lie.TraceForm
LieModule.traceForm_isSymm : ∀ (R : Type u_1) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M],
  LinearMap.IsSymm (LieModule.traceForm R L M)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.map₀MonoidHom_apply : ∀ {ι : 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 ι] [inst_4 : Nonempty ι]
  [inst_5 : (i : ι) → MulOneClass (G i)] [inst_6 : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)]
  (x : (i : ι) → G i), (DirectLimit.map₀MonoidHom f) x = DirectLimit.map₀ f x
-- Init.Grind.Injective
Lean.Grind.leftInv : {α : Sort u} → {β : Sort v} → (f : α → β) → Function.Injective f → [Nonempty α] → β → α
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.closure_empty : ∀ {G : Type u_1} [inst : Group G], Subgroup.closure ∅ = ⊥
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.NonUnitalStarRing.of_apply : ∀ {ι : 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 ι]
  [inst_4 : (i : ι) → NonUnitalNonAssocSemiring (G i)]
  [inst_5 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [inst_6 : (i : ι) → StarRing (G i)]
  [inst_7 : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)] [inst_8 : Nonempty ι] (i : ι) (x : G i),
  (DirectLimit.NonUnitalStarRing.of G f i) x = ⟦⟨i, x⟩⟧
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.IsStableUnderComposition.comp_mem_coverings : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.Precoverage C}
  [self : J.IsStableUnderComposition] {ι : Type (max u v)} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S),
  CategoryTheory.Presieve.ofArrows X f ∈ J.coverings S →
    ∀ {σ : ι → Type (max u v)} {Y : (i : ι) → σ i → C} (g : (i : ι) → (j : σ i) → Y i j ⟶ X i),
      (∀ (i : ι), CategoryTheory.Presieve.ofArrows (Y i) (g i) ∈ J.coverings (X i)) →
        (CategoryTheory.Presieve.ofArrows (fun p => Y p.fst p.snd) fun x =>
            CategoryTheory.CategoryStruct.comp (g x.fst x.snd) (f x.fst)) ∈
          J.coverings S
-- Lean.Elab.Tactic.Try
/-- Return tactics that could solve all subgoals.  -/
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.getTacsSolvedAll : Array (Array (Lean.TSyntax `tactic)) → Array (Lean.TSyntax `tactic)
-- Mathlib.CategoryTheory.ObjectProperty.EpiMono
CategoryTheory.ObjectProperty.prop_X₃_of_shortExact : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderQuotients] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C},
  S.ShortExact → P S.X₂ → P S.X₃
-- Batteries.Lean.NameMapAttribute
/-- This function is called when the attribute is applied.
It should produce a value of type `α` from the given attribute syntax.  -/
Lean.NameMapAttributeImpl.add : {α : Type} → Lean.NameMapAttributeImpl α → Lean.Name → Lean.Syntax → Lean.AttrM α
-- Mathlib.Analysis.Calculus.FDeriv.Pow
/-- Eta-expanded form of `DifferentiableAt.pow` -/
DifferentiableAt.fun_pow : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedAlgebra 𝕜 𝔸] [inst_4 : NormedSpace 𝕜 E] {f : E → 𝔸} {x : E},
  DifferentiableAt 𝕜 f x → ∀ (n : ℕ), DifferentiableAt 𝕜 (fun i => f i ^ n) x
-- Mathlib.Probability.Density
MeasureTheory.pdf_of_not_aemeasurable : ∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {x : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω}
  {μ : MeasureTheory.Measure E} {X : Ω → E}, ¬AEMeasurable X ℙ → MeasureTheory.pdf X ℙ μ =ᵐ[μ] 0
-- Mathlib.Data.Finsupp.ToDFinsupp
toDFinsupp_support : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Zero M] [inst_2 : (m : M) → Decidable (m ≠ 0)]
  (f : ι →₀ M), f.toDFinsupp.support = f.support
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanModuleQuery.mk.sizeOf_spec : ∀ (identifier : String) (openNamespaces : Array Lean.Lsp.OpenNamespace),
  sizeOf { identifier := identifier, openNamespaces := openNamespaces } = 1 + sizeOf identifier + sizeOf openNamespaces
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.aecover_Ici : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : Preorder α] [inst_2 : TopologicalSpace α] [OrderClosedTopology α] [OpensMeasurableSpace α] {a : ι → α},
  Filter.Tendsto a l Filter.atBot → MeasureTheory.AECover μ l fun i => Set.Ici (a i)
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.sumCoords_reindex : ∀ {ι' : Type u_2} {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (b : Module.Basis ι R M) (e : ι ≃ ι'), (b.reindex e).sumCoords = b.sumCoords
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
/-- `ContinuousLinearMap.compContinuousAlternatingMap` as a bundled continuous linear equiv.

Given a continuous linear equivalence `g : F ≃L[𝕜] G`,
this function returns the equivalence between continuous alternating maps with codomain `F`
and continuous alternating maps with codomain `G`
that acts by composing these maps with `g`.
 -/
ContinuousLinearEquiv.continuousAlternatingMapCongrRight : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_4} →
      {G : Type u_5} →
        {ι : Type u_6} →
          [inst : NormedField 𝕜] →
            [inst_1 : AddCommGroup E] →
              [inst_2 : Module 𝕜 E] →
                [inst_3 : TopologicalSpace E] →
                  [inst_4 : AddCommGroup F] →
                    [inst_5 : Module 𝕜 F] →
                      [inst_6 : TopologicalSpace F] →
                        [inst_7 : IsTopologicalAddGroup F] →
                          [inst_8 : ContinuousConstSMul 𝕜 F] →
                            [inst_9 : AddCommGroup G] →
                              [inst_10 : Module 𝕜 G] →
                                [inst_11 : TopologicalSpace G] →
                                  [inst_12 : IsTopologicalAddGroup G] →
                                    [inst_13 : ContinuousConstSMul 𝕜 G] →
                                      (F ≃L[𝕜] G) → E [⋀^ι]→L[𝕜] F ≃L[𝕜] E [⋀^ι]→L[𝕜] G
-- Lean.Meta.SynthInstance
/-- Remark: the SynthInstance.State is not really an extension of `Meta.State`.
The field `postponed` is not needed, and the field `mctx` is misleading since
`synthInstance` methods operate over different `MetavarContext`s simultaneously.
That being said, we still use `extends` because it makes it simpler to move from
`M` to `MetaM`.
 -/
Lean.Meta.SynthInstance.State : Type
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.Ico_add_one_right_eq_Icc_of_not_isMax : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Add α]
  [SuccAddOrder α] {b : α}, ¬IsMax b → ∀ (a : α), Finset.Ico a (b + 1) = Finset.Icc a b
-- Mathlib.Order.Minimal
minimal_ge_iff : ∀ {α : Type u_2} {x y : α} [inst : PartialOrder α], Minimal (fun x => y ≤ x) x ↔ x = y
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {W : CategoryTheory.MorphismProperty C} {X Y Y' : C}
  {f : X ⟶ Y'} {s : Y ⟶ Y'} {hs : W s} {Y'_1 : C} {f_1 : X ⟶ Y'_1} {s_1 : Y ⟶ Y'_1} {hs_1 : W s_1},
  { Y' := Y', f := f, s := s, hs := hs } = { Y' := Y'_1, f := f_1, s := s_1, hs := hs_1 } →
    Y' = Y'_1 ∧ f ≍ f_1 ∧ s ≍ s_1
-- Init.Data.SInt.Lemmas
Int8.add_zero : ∀ (a : Int8), a + 0 = a
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.instIsScalarTower : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] {S : Type u_4}
  {T : Type u_5} [inst_7 : Monoid S] [inst_8 : DistribMulAction S M] [inst_9 : SMulCommClass R S M]
  [inst_10 : LieDerivation.SMulBracketCommClass S L M] [inst_11 : Monoid T] [inst_12 : DistribMulAction T M]
  [inst_13 : SMulCommClass R T M] [inst_14 : LieDerivation.SMulBracketCommClass T L M] [inst_15 : SMul S T]
  [IsScalarTower S T M], IsScalarTower S T (LieDerivation R L M)
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.stieltjesOfMeasurableRat_unit_prod : ∀ {α : Type u_1} {f : α → ℚ → ℝ} [inst : MeasurableSpace α] (hf : Measurable f) (a : α),
  ProbabilityTheory.stieltjesOfMeasurableRat (fun p => f p.2) ⋯ ((), a) =
    ProbabilityTheory.stieltjesOfMeasurableRat f hf a
-- Mathlib.RepresentationTheory.Rep.Iso
Rep.ofModuleMonoidAlgebra.eq_1 : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G],
  Rep.ofModuleMonoidAlgebra =
    { obj := fun M => Rep.of (Representation.ofModule ↑M),
      map := fun {X Y} f =>
        Rep.ofHom
          (let __spread.0 := ModuleCat.Hom.hom f;
          { toAddHom := __spread.0.toAddHom, map_smul' := ⋯, isIntertwining' := ⋯ }),
      map_id := ⋯, map_comp := ⋯ }
-- Init.Data.Rat.Lemmas
Rat.one_den : Rat.den 1 = 1
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.sub_add : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X Y : C}
  (a b c : X ⟶ Y), a - b + c = a - (b - c)
-- Mathlib.Algebra.Category.MonCat.Limits
AddMonCat.forget_createsLimitsOfShape.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J],
  AddMonCat.forget_createsLimitsOfShape = { CreatesLimit := fun {K} => inferInstance }
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
/-- **Alias** of `Matroid.finite_setOfPred_isRestriction`. -/
Matroid.finite_setOf_isRestriction : ∀ {α : Type u_1} (M : Matroid α) [M.Finite], {N | N.IsRestriction M}.Finite
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily_def : ∀ {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] {K : CategoryTheory.GrothendieckTopology D}
  {G : CategoryTheory.Functor C D} {ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)} {ℱ' : CategoryTheory.Sheaf K (Type v)}
  (α : G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) {X : D} (x : ℱ.obj (Opposite.op X)),
  CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily α x = fun x_1 x_2 hf =>
    (CategoryTheory.ConcreteCategory.hom (ℱ'.obj.map (Nonempty.some hf).lift.op))
      ((CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op (Nonempty.some hf).1)))
        ((CategoryTheory.ConcreteCategory.hom (ℱ.map (Nonempty.some hf).map.op)) x))
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Roi.Internal.forIn'_eq_forIn'_iter : ∀ {α : Type u} [inst : LT α] [inst_1 : Std.PRange.UpwardEnumerable α] [inst_2 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_3 : Std.Rxi.IsAlwaysFinite α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ}
  {m : Type u → Type w} [inst_5 : Monad m] {r : Std.Roi α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f = forIn' (Std.Roi.Internal.iter r) init fun a ha acc => f a ⋯ acc
-- Mathlib.FieldTheory.IntermediateField.Algebraic
/-- If `F ≤ E` are two intermediate fields of `L / K` such that `[L : F] = [L : E]` are finite,
then `F = E`.  -/
IntermediateField.eq_of_le_of_finrank_eq' : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {F E : IntermediateField K L}
  [FiniteDimensional (↥F) L], F ≤ E → Module.finrank (↥F) L = Module.finrank (↥E) L → F = E
-- Mathlib.Algebra.CharP.Lemmas
add_pow_prime_pow_eq' : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ},
  Nat.Prime p →
    ∀ (x y : R) (n : ℕ),
      (x + y) ^ p ^ n =
        x ^ p ^ n + y ^ p ^ n + ↑p * ∑ k ∈ Finset.Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p)
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.IsRankOneDiscrete.exists_generator_lt_one : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : Ring A] (v : Valuation A Γ)
  [v.IsRankOneDiscrete], ∃ γ, Subgroup.zpowers γ = (MonoidWithZeroHom.ofClass v).valueGroup ∧ γ < 1
-- Lean.Elab.Tactic.Omega.Core
/-- If we have found a contradiction,
`explanation?` will contain a human readable account of the derivation.
 -/
Lean.Elab.Tactic.Omega.Problem.explanation? : Lean.Elab.Tactic.Omega.Problem → Thunk String
-- Mathlib.InformationTheory.KullbackLeibler.Basic
InformationTheory.klDiv_zero_right : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NeZero μ], InformationTheory.klDiv μ 0 = ⊤
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- The data of an `EffectiveEpi` structure on a `RegularEpi`.  -/
CategoryTheory.effectiveEpiStructOfRegularEpi : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {B X : C} → {f : X ⟶ B} → CategoryTheory.RegularEpi f → CategoryTheory.EffectiveEpiStruct f
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.trailingCoeff_zero : ∀ {R : Type u} [inst : Semiring R], Polynomial.trailingCoeff 0 = 0
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.denom_mul_dvd : ∀ {K : Type u} [inst : Field K] (x y : RatFunc K), (x * y).denom ∣ x.denom * y.denom
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.funUnique_symm_apply : ∀ (α : Type u_2) (M : Type u_4) [inst : Add M] [inst_1 : Unique α] (x : M) (i : α),
  (AddEquiv.funUnique α M).symm x i = x
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.id_s₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C}
  (x : J.ZeroHypercover S) (a : x.I₀), (CategoryTheory.CategoryStruct.id x).s₀ a = a
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.one : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (j : J),
  CommRingCat.Colimits.Relation F (CommRingCat.Colimits.Prequotient.of j 1) CommRingCat.Colimits.Prequotient.one
-- Mathlib.GroupTheory.Commutator.Basic
image_commutatorSet_closureCommutatorRepresentatives : ∀ (G : Type u_1) [inst : Group G],
  ⇑(closureCommutatorRepresentatives G).subtype '' commutatorSet ↥(closureCommutatorRepresentatives G) = commutatorSet G
-- Mathlib.Algebra.Lie.Free
/-- An auxiliary definition used to construct the equivalence `lift` below.  -/
FreeLieAlgebra.liftAux : (R : Type u) →
  {X : Type v} →
    [inst : CommRing R] →
      {L : Type w} →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] → (X → CommutatorRing L) → FreeNonUnitalNonAssocAlgebra R X →ₙₐ[R] CommutatorRing L
-- Std.Data.HashSet.IteratorLemmas
Std.HashSet.toList.eq_1 : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} (m : Std.HashSet α), m.toList = m.inner.keys
-- Init.Data.Fin.Basic
Fin.toNat_eq_val : ∀ {n : ℕ} {i : Fin n}, i.toNat = ↑i
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
_private.Mathlib.CategoryTheory.Limits.Shapes.Reflexive.0.CategoryTheory.Limits.reflexivePair.match_3.eq_3 : ∀ (motive : (X Y : CategoryTheory.Limits.WalkingReflexivePair) → (X ⟶ Y) → Sort u_1)
  (h_1 :
    (x : CategoryTheory.Limits.WalkingReflexivePair) → motive x x (CategoryTheory.Limits.WalkingReflexivePair.Hom.id x))
  (h_2 :
    Unit →
      motive CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.zero
        CategoryTheory.Limits.WalkingReflexivePair.Hom.left)
  (h_3 :
    Unit →
      motive CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.zero
        CategoryTheory.Limits.WalkingReflexivePair.Hom.right)
  (h_4 :
    Unit →
      motive CategoryTheory.Limits.WalkingReflexivePair.zero CategoryTheory.Limits.WalkingReflexivePair.one
        CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion)
  (h_5 :
    Unit →
      motive CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.one
        CategoryTheory.Limits.WalkingReflexivePair.Hom.rightCompReflexion)
  (h_6 :
    Unit →
      motive CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.one
        CategoryTheory.Limits.WalkingReflexivePair.Hom.leftCompReflexion),
  (match CategoryTheory.Limits.WalkingReflexivePair.one, CategoryTheory.Limits.WalkingReflexivePair.zero,
      CategoryTheory.Limits.WalkingReflexivePair.Hom.right with
    | x, .(x), CategoryTheory.Limits.WalkingReflexivePair.Hom.id .(x) => h_1 x
    | .(CategoryTheory.Limits.WalkingReflexivePair.one), .(CategoryTheory.Limits.WalkingReflexivePair.zero),
      CategoryTheory.Limits.WalkingReflexivePair.Hom.left => h_2 ()
    | .(CategoryTheory.Limits.WalkingReflexivePair.one), .(CategoryTheory.Limits.WalkingReflexivePair.zero),
      CategoryTheory.Limits.WalkingReflexivePair.Hom.right => h_3 ()
    | .(CategoryTheory.Limits.WalkingReflexivePair.zero), .(CategoryTheory.Limits.WalkingReflexivePair.one),
      CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion => h_4 ()
    | .(CategoryTheory.Limits.WalkingReflexivePair.one), .(CategoryTheory.Limits.WalkingReflexivePair.one),
      CategoryTheory.Limits.WalkingReflexivePair.Hom.rightCompReflexion => h_5 ()
    | .(CategoryTheory.Limits.WalkingReflexivePair.one), .(CategoryTheory.Limits.WalkingReflexivePair.one),
      CategoryTheory.Limits.WalkingReflexivePair.Hom.leftCompReflexion => h_6 ()) =
    h_3 ()
-- Init.Data.Slice.Array.Lemmas
Array.size_mkSlice_ric : ∀ {α : Type u_1} {xs : Array α} {hi : ℕ}, Std.Slice.size (Std.Ric.Sliceable.mkSlice xs *...=hi) = min (hi + 1) xs.size
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.decompose_smul : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (ℳ : ι → Submodule R M) [inst_4 : DirectSum.Decomposition ℳ] (r : R) (x : M),
  (DirectSum.decompose ℳ) (r • x) = r • (DirectSum.decompose ℳ) x
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.isUnit_inl_iff : ∀ {R : Type u} {M : Type v} [inst : AddCommGroup M] [inst_1 : Semiring R] [inst_2 : Module Rᵐᵒᵖ M] [inst_3 : Module R M]
  [inst_4 : SMulCommClass R Rᵐᵒᵖ M] {r : R}, IsUnit (TrivSqZeroExt.inl r) ↔ IsUnit r
-- Init.Data.SInt.Lemmas
Int64.lt_iff_toInt_lt : ∀ {x y : Int64}, x < y ↔ x.toInt < y.toInt
-- Mathlib.LinearAlgebra.Pi
Submodule.iSup_map_single : ∀ {R : Type u} {ι : Type x} [inst : Semiring R] {φ : ι → Type u_1} [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] {p : (i : ι) → Submodule R (φ i)} [inst_3 : DecidableEq ι] [Finite ι],
  ⨆ i, Submodule.map (LinearMap.single R φ i) (p i) = Submodule.pi Set.univ p
-- Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
/-- If a category has all binary coproducts and all coequalizers, then it also has all pushouts.
As usual, this is not an instance, since there may be a more direct way to construct pushouts.  -/
CategoryTheory.Limits.hasPushouts_of_hasBinaryCoproducts_of_hasCoequalizers : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C]
  [CategoryTheory.Limits.HasCoequalizers C], CategoryTheory.Limits.HasPushouts C
-- Mathlib.RingTheory.TwoSidedIdeal.Kernel
/-- The kernel of the ring homomorphism `R → R⧸I` is `I`.
 -/
TwoSidedIdeal.ker_ringCon_mk' : ∀ {R : Type u_4} [inst : NonAssocRing R] (I : TwoSidedIdeal R), TwoSidedIdeal.ker I.ringCon.mk' = I
-- Mathlib.Topology.MetricSpace.Completion
Isometry.completion_extension : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] [CompleteSpace β] [T0Space β]
  {f : α → β}, Isometry f → Isometry (UniformSpace.Completion.extension f)
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyWith.coe_toContinuousMap : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  {P : C(X, Y) → Prop} (F : f₀.HomotopyWith f₁ P), ⇑F.toContinuousMap = ⇑F
-- Mathlib.Analysis.Matrix.Normed
/-- Normed ring instance (using sup norm of L1 norm) for matrices over a normed ring.  Not
declared as an instance because there are several natural choices for defining the norm of a
matrix.  -/
Matrix.linftyOpNormedRing : {n : Type u_4} → {α : Type u_5} → [Fintype n] → [NormedRing α] → [DecidableEq n] → NormedRing (Matrix n n α)
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
/-- An equivalence between an `IsAddKleinFour` group `G₁` and a group `G₂` of exponent
two which sends `0 : G₁` to `0 : G₂` is in fact an isomorphism.  -/
IsAddKleinFour.addEquiv' : {G₁ : Type u_2} →
  {G₂ : Type u_3} →
    [inst : AddGroup G₁] →
      [inst_1 : AddGroup G₂] → [IsAddKleinFour G₁] → (e : G₁ ≃ G₂) → e 0 = 0 → AddMonoid.exponent G₂ = 2 → G₁ ≃+ G₂
-- Mathlib.Data.Finsupp.Antidiagonal
Finsupp.antidiagonal_single : ∀ {α : Type u} [inst : DecidableEq α] (a : α) (n : ℕ),
  (Finset.HasAntidiagonal.antidiagonal fun₀ | a => n) =
    Finset.map ({ toFun := Finsupp.single a, inj' := ⋯ }.prodMap { toFun := Finsupp.single a, inj' := ⋯ })
      (Finset.HasAntidiagonal.antidiagonal n)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k},
  (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.minKey? =
    some (t.minKey?.elim k fun k' => if (compare k k').isLE = true then k else k')
-- Mathlib.RingTheory.Flat.Tensor
/-- The `lTensor`-variant of `iff_rTensor_injective'`. .  -/
Module.Flat.iff_lTensor_injective' : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(LinearMap.lTensor M (Submodule.subtype I))
-- Mathlib.Algebra.Order.GroupWithZero.Defs
mul_lt_mul_of_le_of_lt_of_nonneg_of_pos : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c d : α} [PosMulStrictMono α]
  [MulPosMono α], a ≤ b → c < d → 0 ≤ c → 0 < b → a * c < b * d
-- Std.Do.Triple.SpecLemmas
/-- Creates a cursor at the beginning of the list (position 0).
The prefix is empty and the suffix is the entire list.
 -/
List.Cursor.begin : {α : Type u_1} → (l : List α) → l.Cursor
-- Lean.Meta.Tactic.UnifyEq
Lean.Meta.UnifyEqResult.numNewEqs : Lean.Meta.UnifyEqResult → ℕ
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.adjugate_fin_three : ∀ {α : Type w} [inst : CommRing α] (A : Matrix (Fin 3) (Fin 3) α),
  A.adjugate =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
      -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
      A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]
-- Mathlib.Order.Circular
CircularPreorder.toSBtw : {α : Type u_1} → [self : CircularPreorder α] → SBtw α
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.toTopologicalSpace_iInf : ∀ {α : Type u} [inst : AddGroup α] {ι : Sort u_1} (s : ι → AddGroupTopology α),
  (⨅ i, s i).toTopologicalSpace = ⨅ i, (s i).toTopologicalSpace
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.transfer.eq_1 : ∀ {V : Type u} {G : SimpleGraph V} {u : V} (H : SimpleGraph V) (h_2 : ∀ e ∈ SimpleGraph.Walk.nil.edges, e ∈ H.edgeSet),
  SimpleGraph.Walk.nil.transfer H h_2 = SimpleGraph.Walk.nil