mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.CommMon_
/-- Constructor for morphisms in `CommMon C`.  -/
CategoryTheory.CommMon.homMk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → {A B : CategoryTheory.CommMon C} → (A.toMon ⟶ B.toMon) → (A ⟶ B)
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.p_def : ∀ {α : Type u_2} [inst : Fintype α] (a b : α → ℝ),
  AkraBazziRecurrence.p a b = Function.invFun (fun p => ∑ i, a i * b i ^ p) 1
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.grevlex.eq_1 : ∀ (m₁ m₂ : Lean.Grind.CommRing.Mon), m₁.grevlex m₂ = (compare m₁.degree m₂.degree).then (m₁.revlex m₂)
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
/-- A continuous affine equivalence is a homeomorphism.  -/
ContinuousAffineEquiv.toHomeomorph : {k : Type u_1} →
  {P₁ : Type u_2} →
    {P₂ : Type u_3} →
      {V₁ : Type u_6} →
        {V₂ : Type u_7} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V₁] →
              [inst_2 : Module k V₁] →
                [inst_3 : AddTorsor V₁ P₁] →
                  [inst_4 : TopologicalSpace P₁] →
                    [inst_5 : AddCommGroup V₂] →
                      [inst_6 : Module k V₂] →
                        [inst_7 : AddTorsor V₂ P₂] → [inst_8 : TopologicalSpace P₂] → (P₁ ≃ᴬ[k] P₂) → P₁ ≃ₜ P₂
-- Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
/-- For `P` a family of measures, with `P J` a measure on `Π j : J, α j`, we define a function
`projectiveFamilyFun P s` by setting it to `P I S` if `s = cylinder I S` for a measurable `S` and
to 0 if `s` is not a measurable cylinder.  -/
MeasureTheory.projectiveFamilyFun : {ι : Type u_1} →
  {α : ι → Type u_2} →
    {mα : (i : ι) → MeasurableSpace (α i)} →
      ((J : Finset ι) → MeasureTheory.Measure ((j : ↥J) → α ↑j)) → Set ((i : ι) → α i) → ENNReal
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.adjugate_def : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α),
  A.adjugate = Matrix.of fun i => A.transpose.cramer (Pi.single i 1)
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
/-- Denominator of an element in `HomogeneousLocalization x`.  -/
HomogeneousLocalization.den : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] → [inst_1 : SetLike σ A] → {𝒜 : ι → σ} → {x : Submonoid A} → HomogeneousLocalization 𝒜 x → A
-- Init.Data.Range.Polymorphic.Int
Std.PRange.instLawfulHasSizeInt : Std.Rxc.LawfulHasSize ℤ
-- Init.Data.List.TakeDrop
List.take_eq_nil_of_eq_nil : ∀ {α : Type u_1} {as : List α} {i : ℕ}, as = [] → List.take i as = []
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.symm_bijective : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β],
  Function.Bijective MeasurableEquiv.symm
-- Init.Data.Range.Basic
Std.Legacy.Range.instForIn'NatInferInstanceMembershipOfMonad : {m : Type u_1 → Type u_2} → [Monad m] → ForIn' m Std.Legacy.Range ℕ inferInstance
-- Init.System.IO
/-- Returns the current state of a task in the Lean runtime's task manager.

For tasks derived from `Promise`s, the states `waiting` and `running` should be considered
equivalent.
 -/
IO.getTaskState : {α : Type u_1} → Task α → BaseIO IO.TaskState
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.setValue_right_apply_eq : ∀ {α : Sort u_1} {β : Sort u_2} (f : α ↪ β) (a c : α) [inst : (a' : α) → Decidable (a' = a)]
  [inst_1 : (a' : α) → Decidable (f a' = f c)], (f.setValue a (f c)) c = f a
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.T.eq_3 : ∀ (R : Type u_1) [inst : CommRing R] (n : ℕ),
  Polynomial.Chebyshev.T R (Int.ofNat n.succ.succ) =
    2 * Polynomial.X * Polynomial.Chebyshev.T R (↑n + 1) - Polynomial.Chebyshev.T R ↑n
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.ofRat_mul : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (x y : β),
  CauSeq.Completion.ofRat (x * y) = CauSeq.Completion.ofRat x * CauSeq.Completion.ofRat y
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.toSheafify_naturality_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) {Z : CategoryTheory.Functor Cᵒᵖ D}
  (h : CategoryTheory.sheafify J Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J Q) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J P)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyMap J η) h)
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.Disjoint.inv_left : ∀ {α : Type u_1} {f g : Equiv.Perm α}, f.Disjoint g → f⁻¹.Disjoint g
-- Init.Data.UInt.Bitwise
UInt64.shiftRight_and : ∀ {a b c : UInt64}, (a &&& b) >>> c = a >>> c &&& b >>> c
-- Mathlib.Algebra.Group.Commute.Basic
AddSemiconjBy.function_semiconj_add_left : ∀ {G : Type u_1} [inst : AddSemigroup G] {a b c : G},
  AddSemiconjBy a b c → Function.Semiconj (fun x => a + x) (fun x => b + x) fun x => c + x
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k : α},
  (Std.ExtHashMap.filterMap f m)[k]? = m[k]?.pbind fun x_2 h' => f (m.getKey k ⋯) x_2
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEmbedding.equivRange.congr_simp : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : α → β}
  (hf : MeasurableEmbedding f), hf.equivRange = hf.equivRange
-- Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Polynomial.scaleRoots.isWeaklyEisensteinAt : ∀ {R : Type u} [inst : CommRing R] (p : Polynomial R) {x : R} {P : Ideal R},
  x ∈ P → (p.scaleRoots x).IsWeaklyEisensteinAt P
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the reverse direction of `le_sub_iff_add_le`. -/
le_sub_right_of_add_le : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddRightMono α] {a b c : α}, a + b ≤ c → a ≤ c - b
-- Batteries.Data.Nat.Bisect
Nat.bisect_add_one_false : ∀ {start stop : ℕ} {p : ℕ → Bool} (h : start < stop) (hstart : p start = true) (hstop : p stop = false),
  p (Nat.bisect h hstart hstop + 1) = false
-- Mathlib.Analysis.SpecialFunctions.Log.Base
/-- The real logarithm base b is continuous as a function from positive reals.  -/
Real.continuous_logb' : ∀ {b : ℝ}, Continuous fun x => Real.logb b ↑x
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.coconeOfPredicateSet_ι_app : ∀ {α : PartOrdEmb} (P : Set ↑α → Prop) (J : Subtype P),
  (PartOrdEmb.coconeOfPredicateSet P).ι.app J = PartOrdEmb.ofHom (OrderEmbedding.subtype fun x => x ∈ ↑J)
-- Init.Data.Slice.List.Basic
instSliceableListNatListSlice_6 : {α : Type u} → Std.Ric.Sliceable (List α) ℕ (ListSlice α)
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.card_preOmega : ∀ (o : Ordinal.{u_1}), (Ordinal.preOmega o).card = Cardinal.preAleph o
-- Mathlib.LinearAlgebra.Dual.Basis
Module.Basis.toDual_apply_left : ∀ {R : Type uR} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : DecidableEq ι] (b : Module.Basis ι R M) (m : M) (i : ι), (b.toDual m) (b i) = (b.repr m) i
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
ProbabilityTheory.Kernel.instIsMarkovKernelCondKernelUnitReal : ∀ {α : Type u_1} {mα : MeasurableSpace α} (κ : ProbabilityTheory.Kernel Unit (α × ℝ))
  [inst : ProbabilityTheory.IsFiniteKernel κ], ProbabilityTheory.IsMarkovKernel κ.condKernelUnitReal
-- Mathlib.Util.Export
Lean.Export.exportDef : Lean.Name → Lean.ExportM Unit
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.HasImageMap.imageMap.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  [inst_1 : CategoryTheory.Limits.HasImage f.hom] [inst_2 : CategoryTheory.Limits.HasImage g.hom] (sq : f ⟶ g)
  [inst_3 : CategoryTheory.Limits.HasImageMap sq],
  CategoryTheory.Limits.HasImageMap.imageMap sq = CategoryTheory.Limits.HasImageMap.imageMap sq
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_empty : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {a fallback : α}, ∅.getKeyD a fallback = fallback
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.N.mk'.congr_simp : ∀ {X : SSet} (toS toS_1 : X.S) (e_toS : toS = toS_1) (nonDegenerate : toS.simplex ∈ X.nonDegenerate toS.dim),
  { toS := toS, nonDegenerate := nonDegenerate } = { toS := toS_1, nonDegenerate := ⋯ }
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.map_le_range : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N) (H : AddSubgroup G),
  AddSubgroup.map f H ≤ f.range
-- Mathlib.Order.Cover
covBy_iff_wcovBy_and_ne : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ⋖ b ↔ a ⩿ b ∧ a ≠ b
-- Mathlib.RingTheory.DividedPowers.DPMorphism
DividedPowers.DPMorphism.mk : {A : Type u_3} →
  {B : Type u_4} →
    [inst : CommSemiring A] →
      [inst_1 : CommSemiring B] →
        {I : Ideal A} →
          {J : Ideal B} →
            {hI : DividedPowers I} →
              {hJ : DividedPowers J} →
                (toRingHom : A →+* B) →
                  Ideal.map toRingHom I ≤ J →
                    (∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom a) = toRingHom (hI.dpow n a)) → hI.DPMorphism hJ
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.instNoZeroDivisors : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M], NoZeroDivisors (Associates M)
-- Mathlib.CategoryTheory.CodiscreteCategory
CategoryTheory.Codiscrete.natIsoFunctor_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type w}
  {F : CategoryTheory.Functor C (CategoryTheory.Codiscrete A)} (X : C),
  CategoryTheory.Codiscrete.natIsoFunctor.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
-- Mathlib.RingTheory.Ideal.Basic
/-- When a ring is not a field, the maximal ideals are nontrivial.  -/
Ring.ne_bot_of_isMaximal_of_not_isField : ∀ {R : Type u_5} [inst : CommSemiring R] [Nontrivial R] {M : Ideal R}, M.IsMaximal → ¬IsField R → M ≠ ⊥
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.toSubmodule_eq_top : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M), ↑N = ⊤ ↔ N = ⊤
-- Init.Data.UInt.Bitwise
UInt16.neg_one_and : ∀ {a : UInt16}, -1 &&& a = a
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_range_le : ∀ {α β : Type u} {f : α → β}, Cardinal.mk ↑(Set.range f) ≤ Cardinal.mk α
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.IsAcyclic.eq_penultimate_of_adj_end : ∀ {V : Type u_1} {G : SimpleGraph V},
  G.IsAcyclic → ∀ {u v w : V} {p : G.Walk u v}, p.IsPath → G.Adj v w → w ∈ p.support → w = p.penultimate
-- Mathlib.Algebra.Order.Group.Abs
eq_of_abs_sub_eq_zero : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] {a b : G}, |a - b| = 0 → a = b
-- Mathlib.RingTheory.KrullDimension.NonZeroDivisors
ringKrullDim_mvPolynomial_of_isEmpty : ∀ {R : Type u_1} [inst : CommRing R] (σ : Type u_3) [IsEmpty σ], ringKrullDim (MvPolynomial σ R) = ringKrullDim R
-- Mathlib.FieldTheory.RatFunc.Degree
RatFunc.natDegree_num_mul_right_sub_natDegree_denom_mul_left_eq_intDegree : ∀ {K : Type u} [inst : Field K] {x : RatFunc K},
  x ≠ 0 → ∀ {s : Polynomial K}, s ≠ 0 → ↑(x.num * s).natDegree - ↑(s * x.denom).natDegree = x.intDegree
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.v : Std.Time.GenericFormat.DateBuilder✝ → Option String
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Substructure.FG.cg : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] {N : L.Substructure M}, N.FG → N.CG
-- Mathlib.Analysis.Normed.Group.Basic
norm_le_mul_norm_add : ∀ {E : Type u_5} [inst : SeminormedGroup E] (u v : E), ‖u‖ ≤ ‖u * v‖ + ‖v‖
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.subtype_comp_rangeRestrict : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N),
  f.range.subtype.comp f.rangeRestrict = f
-- Mathlib.Data.List.SplitBy
List.splitBy_append_cons : ∀ {α : Type u_1} {r : α → α → Bool} {l : List α} {a : α} (m : List α),
  (∀ x ∈ l.getLast?, r x a = false) → List.splitBy r (l ++ a :: m) = List.splitBy r l ++ List.splitBy r (a :: m)
-- Init.Grind.Ordered.Field
Lean.Grind.Field.IsOrdered.le_mul_inv_iff_le_mul_of_neg : ∀ {R : Type u} [inst : Lean.Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] (a b : R) {c : R}, c < 0 → (a ≤ b * c⁻¹ ↔ b ≤ a * c)
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.isLeftDescent_iff : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w : W} {i : B},
  cs.IsLeftDescent w i ↔ cs.length (cs.simple i * w) + 1 = cs.length w
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.rotCompInvRot_hom_app_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  (CategoryTheory.Pretriangulated.rotCompInvRot.hom.app X).hom₂ = CategoryTheory.CategoryStruct.id X.obj₂
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.congr_simp : ∀ (κ κ_1 : Cardinal.{u}) (e_κ : κ = κ_1) [inst : Fact κ.IsRegular],
  CategoryTheory.CardinalDirectedPoset κ = CategoryTheory.CardinalDirectedPoset κ_1
-- Init.Data.String.Lemmas.Basic
String.cast_pos : ∀ {s t : String} {p : String.Pos.Raw} {h : String.Pos.Raw.IsValid s p} {h' : s = t}, (s.pos p h).cast h' = t.pos p ⋯
-- Mathlib.Topology.Homotopy.Lifting
/-- The fundamental group of the base of simply-connected covering map is contravariantly
equivalent to the group of the covering map.  -/
IsQuotientCoveringMap.fundamentalGroupEquiv : {E : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace E] →
      [inst_1 : TopologicalSpace X] →
        {p : E → X} →
          {G : Type u_4} →
            [inst_2 : Group G] →
              [inst_3 : MulAction G E] →
                IsQuotientCoveringMap p G →
                  {x : X} → ↑(p ⁻¹' {x}) → [SimplyConnectedSpace E] → FundamentalGroup X x ≃* Gᵐᵒᵖ
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.comp' : ∀ {n m : ℕ} {f : List.Vector ℕ m → ℕ} {g : List.Vector ℕ n → List.Vector ℕ m},
  Nat.Primrec' f → Nat.Primrec'.Vec g → Nat.Primrec' fun v => f (g v)
-- Mathlib.Data.Multiset.AddSub
Multiset.add_sub_cancel_right : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, s + t - t = s
-- Mathlib.Topology.Sober
genericPoints_eq_singleton : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : QuasiSober α] [inst_2 : IrreducibleSpace α] [T0Space α],
  genericPoints α = {genericPoint α}
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
/-- Given a partition `π` of `I : BoxIntegral.Box ι` and a collection of tagged partitions
`πi J` of all boxes `J ∈ π`, returns the tagged partition of `I` into all the boxes of `πi J`
with tags coming from `(πi J).tag`.  -/
BoxIntegral.Prepartition.biUnionTagged : {ι : Type u_1} →
  {I : BoxIntegral.Box ι} →
    BoxIntegral.Prepartition I →
      ((J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J) → BoxIntegral.TaggedPrepartition I
-- Mathlib.Algebra.Homology.DifferentialObject
CategoryTheory.DifferentialObject.d_squared_apply_assoc : ∀ {β : Type u_1} [inst : AddCommGroup β] {b : β} {V : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} V]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V]
  (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) {x : β} {Z : V}
  (h : (CategoryTheory.shiftFunctor (CategoryTheory.GradedObjectWithShift b V) 1).obj X.obj (x + 1 • b) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.d x) (CategoryTheory.CategoryStruct.comp (X.d (x + 1 • b)) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Tactic.Translate.Reorder
Mathlib.Tactic.Translate.ArgReorder.brecOn_1.eq : ∀ {motive_1 : Mathlib.Tactic.Translate.ArgReorder → Sort u}
  {motive_2 : Array (ℕ × Mathlib.Tactic.Translate.ArgReorder) → Sort u}
  {motive_3 : List (ℕ × Mathlib.Tactic.Translate.ArgReorder) → Sort u}
  {motive_4 : ℕ × Mathlib.Tactic.Translate.ArgReorder → Sort u} (t : Array (ℕ × Mathlib.Tactic.Translate.ArgReorder))
  (F_1 : (t : Mathlib.Tactic.Translate.ArgReorder) → t.below → motive_1 t)
  (F_2 :
    (t : Array (ℕ × Mathlib.Tactic.Translate.ArgReorder)) → Mathlib.Tactic.Translate.ArgReorder.below_1 t → motive_2 t)
  (F_3 :
    (t : List (ℕ × Mathlib.Tactic.Translate.ArgReorder)) → Mathlib.Tactic.Translate.ArgReorder.below_2 t → motive_3 t)
  (F_4 : (t : ℕ × Mathlib.Tactic.Translate.ArgReorder) → Mathlib.Tactic.Translate.ArgReorder.below_3 t → motive_4 t),
  Mathlib.Tactic.Translate.ArgReorder.brecOn_1 t F_1 F_2 F_3 F_4 =
    F_2 t (Mathlib.Tactic.Translate.ArgReorder.brecOn_1.go t F_1 F_2 F_3 F_4).2
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getD_map : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {γ : α → Type w}
  [inst : LawfulBEq α] {f : (a : α) → β a → γ a} {k : α} {fallback : γ k},
  (Std.ExtDHashMap.map f m).getD k fallback = (Option.map (f k) (m.get? k)).getD fallback
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.modEq_iff_zsmul' : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a b : G}, a ≡ b [PMOD p] ↔ ∃ m, b - a = m • p
-- Init.Data.Nat.Basic
Nat.pow_one : ∀ (a : ℕ), a ^ 1 = a
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.map_closure : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] (f : L.Hom M N)
  (s : Set M),
  FirstOrder.Language.Substructure.map f ((FirstOrder.Language.Substructure.closure L).toFun s) =
    (FirstOrder.Language.Substructure.closure L).toFun (⇑f '' s)
-- Mathlib.Order.Concept
Concept.extent_ofIsIntent : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : Set β) (ht : Order.IsIntent r t),
  (Concept.ofIsIntent r t ht).extent = lowerPolar r t
-- Mathlib.Analysis.Normed.Group.Defs
ENormedCommMonoid.toENormedMonoid : {E : Type u_8} → [inst : TopologicalSpace E] → [self : ENormedCommMonoid E] → ENormedMonoid E
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.num_one : ∀ {K : Type u} [inst : Field K], RatFunc.num 1 = 1
-- Std.Net.Addr
Std.Net.IPv6Addr.mk.inj : ∀ {segments segments_1 : Vector UInt16 8}, { segments := segments } = { segments := segments_1 } → segments = segments_1
-- Mathlib.Topology.Homotopy.Basic
/-- value of the homotopy at 0  -/
ContinuousMap.Homotopy.map_zero_left : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  (self : f₀.Homotopy f₁) (x : X), self.toFun (0, x) = f₀ x
-- Mathlib.FieldTheory.Differential.Basic
Differential.logDeriv_eq_zero : ∀ {R : Type u_1} [inst : Field R] [inst_1 : Differential R] (a : R), Differential.logDeriv a = 0 ↔ a′ = 0
-- Mathlib.Data.Matrix.PEquiv
PEquiv.mul_toMatrix_toPEquiv : ∀ {l : Type u_2} {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : DecidableEq n]
  [inst_2 : NonAssocSemiring α] (M : Matrix l m α) (f : m ≃ n), M * f.toPEquiv.toMatrix = M.submatrix id ⇑f.symm
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.Embedding.instIsRelIffOp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [e.IsRelIff],
  e.op.IsRelIff
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {T X Y : C} {f g : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y},
  f = g ↔
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y) =
        CategoryTheory.CategoryStruct.comp g (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y) ∧
      CategoryTheory.CategoryStruct.comp f (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y) =
        CategoryTheory.CategoryStruct.comp g (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y)
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.leadingCoeff_C : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] (c : R),
  m.leadingCoeff (MvPolynomial.C c) = c
-- Mathlib.Computability.NFA
NFA.accepts_eq_acceptsFrom_start : ∀ {α : Type u} {σ : Type v} {M : NFA α σ}, M.accepts = M.acceptsFrom M.start
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivAt.congr_of_eventuallyEq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f f₁ : 𝕜 → F} {f' : F} {x : 𝕜}, HasDerivAt f f' x → f₁ =ᶠ[nhds x] f → HasDerivAt f₁ f' x
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.BundledIterM.inst : {m : Type w → Type w'} → {β : Type w} → (self : Std.BundledIterM m β) → Std.Iterator self.α m β
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.compLeftMonoidHom.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} (N : Type u_6) [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {E'' : Type u_7} [inst_9 : NormedAddCommGroup E''] [inst_10 : NormedSpace 𝕜 E''] {H'' : Type u_8}
  [inst_11 : TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''} {n : WithTop ℕ∞} {G' : Type u_10}
  [inst_12 : Monoid G'] [inst_13 : TopologicalSpace G'] [inst_14 : ChartedSpace H' G'] [inst_15 : ContMDiffMul I' n G']
  {G'' : Type u_11} [inst_16 : Monoid G''] [inst_17 : TopologicalSpace G''] [inst_18 : ChartedSpace H'' G'']
  [inst_19 : ContMDiffMul I'' n G''] (φ : G' →* G'') (hφ : ContMDiff I' I'' n ⇑φ),
  ContMDiffMap.compLeftMonoidHom I N φ hφ = { toFun := fun f => ⟨⇑φ ∘ ⇑f, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.GroupTheory.RegularWreathProduct
RegularWreathProduct.left_inl : ∀ {D : Type u_1} {Q : Type u_2} [inst : Group D] [inst_1 : Group Q] (q : Q), (RegularWreathProduct.inl q).left = 1
-- Mathlib.Topology.PartitionOfUnity
BumpCovering.sum_toPOUFun_eq : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (x : X),
  ∑ᶠ (i : ι), f.toPOUFun i x = 1 - ∏ᶠ (i : ι), (1 - (f i) x)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPullback.of_isLimit_binaryFan_of_isTerminal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {c : CategoryTheory.Limits.BinaryFan X Y}
  (hc : CategoryTheory.Limits.IsLimit c) {T : C} (hT : CategoryTheory.Limits.IsTerminal T),
  CategoryTheory.IsPullback c.fst c.snd
    (hT.from ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left }))
    (hT.from ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right }))
-- Mathlib.Algebra.Algebra.Basic
/-- This references the `ULift.algebra'` instance.  -/
ULift.algebraMap_apply' : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (r : ULift.{u_4, u_1} R), (algebraMap (ULift.{u_4, u_1} R) A) r = (algebraMap R A) r.down
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.coeff_monomial_succ : ∀ {R : Type u_1} {n : ℕ} [inst : Semiring R] {a : R}, ((SkewPolynomial.monomial (n + 1)) a).coeff 0 = 0