mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.coeff_mapRingEquiv : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Monoid M]
  (e : R ≃+* S) (x : MonoidAlgebra R M) (m : M), ((MonoidAlgebra.mapRingEquiv M e) x).coeff m = e (x.coeff m)
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.associator_hom_inv : ∀ {B : Type u} [inst : Quiver B] {a b c d : B} (f : CategoryTheory.FreeBicategory.Hom a b)
  (g : CategoryTheory.FreeBicategory.Hom b c) (h : CategoryTheory.FreeBicategory.Hom c d),
  CategoryTheory.FreeBicategory.Rel
    ((CategoryTheory.FreeBicategory.Hom₂.associator f g h).vcomp
      (CategoryTheory.FreeBicategory.Hom₂.associator_inv f g h))
    (CategoryTheory.FreeBicategory.Hom₂.id ((f.comp g).comp h))
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.inf_mul_assoc : ∀ {G : Type u_2} [inst : Group G] (A B C : Subgroup G), C ≤ A → ↑(A ⊓ B) * ↑C = ↑A ∩ (↑B * ↑C)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_insertIfNew! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k a : α} {fallback v : β},
      Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.insertIfNew! k v t) a fallback =
        if compare k a = Ordering.eq ∧ k ∉ t then v else Std.DTreeMap.Internal.Impl.Const.getD t a fallback
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.mono_g_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C}, S.Exact → (CategoryTheory.Mono S.g ↔ S.f = 0)
-- Mathlib.CategoryTheory.Category.Pairwise
_private.Mathlib.CategoryTheory.Category.Pairwise.0.CategoryTheory.instFintypePairwise.match_5.splitter : (ι : Type u_1) →
  (motive : CategoryTheory.Pairwise ι → Sort u_2) →
    (x : CategoryTheory.Pairwise ι) →
      ((a : ι) → motive (CategoryTheory.Pairwise.single a)) →
        ((a a_1 : ι) → motive (CategoryTheory.Pairwise.pair a a_1)) → motive x
-- Std.Do.PredTrans
Std.Do.PredTrans.mono : ∀ {ps : Std.Do.PostShape} {α : Type u} (t : Std.Do.PredTrans ps α), Std.Do.PredTrans.Monotonic t.apply
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
SymmetricAlgebra.algebraMap_leftInverse : ∀ {R : Type u_1} (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Function.LeftInverse ⇑SymmetricAlgebra.algebraMapInv ⇑(algebraMap R (SymmetricAlgebra R M))
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.swap_obj_toProd : ∀ (X : Bipointed), (Bipointed.swap.obj X).toProd = X.toProd.swap
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.prodEquiv_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : Star B] [inst_7 : NonUnitalNonAssocSemiring C]
  [inst_8 : DistribMulAction R C] [inst_9 : Star C] (f : (A →⋆ₙₐ[R] B) × (A →⋆ₙₐ[R] C)),
  NonUnitalStarAlgHom.prodEquiv f = f.1.prod f.2
-- Mathlib.Data.Sign.Defs
SignType.instOne : One SignType
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_inter_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∉ t₂ → (t₁ ∩ t₂).get? k = none
-- Std.Data.DHashMap.Raw
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise `none`.
The result in the `some` case is guaranteed to be pointer equal to the key in the map.
 -/
Std.DHashMap.Raw.getKey? : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable α] → Std.DHashMap.Raw α β → α → Option α
-- Lean.Parser.Extension
/-- If the parsing stack ends with an the option name and value, then the option is set in the context
while parsing `p`. The value is the top of the stack and the name is the identifier two entries
below it.
 -/
Lean.Parser.withSetOptionValueFn : Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.Analysis.RCLike.Basic
RCLike.real_smul_eq_coe_smul : ∀ {K : Type u_1} {E : Type u_2} [inst : RCLike K] [inst_1 : AddCommGroup E] [inst_2 : Module K E] [inst_3 : Module ℝ E]
  [IsScalarTower ℝ K E] (r : ℝ) (x : E), r • x = ↑r • x
-- Mathlib.Analysis.Normed.Field.Basic
dist_inv_inv₀ : ∀ {α : Type u_2} [inst : NormedDivisionRing α] {z w : α}, z ≠ 0 → w ≠ 0 → dist z⁻¹ w⁻¹ = dist z w / (‖z‖ * ‖w‖)
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.div_sub_div_of_dvd : ∀ {R : Type u} [inst : EuclideanDomain R] {x y z t : R},
  y ≠ 0 → t ≠ 0 → y ∣ x → t ∣ z → x / y - z / t = (t * x - y * z) / (t * y)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.pullbackMap.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y Z X : C} (f : Y ⟶ X) (g : Z ⟶ X)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g] {Y' Z' X' : C} (f' : Y' ⟶ X') (g' : Z' ⟶ X')
  [inst_2 : CategoryTheory.ChosenPullbacksAlong g'] (γ₁ γ₁_1 : Y' ⟶ Y) (e_γ₁ : γ₁ = γ₁_1) (γ₂ γ₂_1 : Z' ⟶ Z)
  (e_γ₂ : γ₂ = γ₂_1) (γ₃ γ₃_1 : X' ⟶ X) (e_γ₃ : γ₃ = γ₃_1)
  (comm₁ : CategoryTheory.CategoryStruct.comp f' γ₃ = CategoryTheory.CategoryStruct.comp γ₁ f)
  (comm₂ : CategoryTheory.CategoryStruct.comp g' γ₃ = CategoryTheory.CategoryStruct.comp γ₂ g),
  CategoryTheory.ChosenPullbacksAlong.pullbackMap f g f' g' γ₁ γ₂ γ₃ comm₁ comm₂ =
    CategoryTheory.ChosenPullbacksAlong.pullbackMap f g f' g' γ₁_1 γ₂_1 γ₃_1 ⋯ ⋯
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_eq_some_get : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {a : α} (h : a ∈ t), Std.ExtDTreeMap.Const.get? t a = some (Std.ExtDTreeMap.Const.get t a h)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
Lean.Meta.Grind.Arith.CommRing.getRingId : Lean.Meta.Grind.Arith.CommRing.RingM ℕ
-- Mathlib.Logic.Equiv.Basic
Equiv.piCongrRight_apply : ∀ {α : Sort u_1} {β₁ : α → Sort u_9} {β₂ : α → Sort u_10} (F : (a : α) → β₁ a ≃ β₂ a) (a : (i : α) → β₁ i) (i : α),
  (Equiv.piCongrRight F) a i = Pi.map (fun a => ⇑(F a)) a i
-- Mathlib.Order.Preorder.Chain
Flag.instUnique : {α : Type u_1} → [inst : LinearOrder α] → Unique (Flag α)
-- Mathlib.Order.BooleanAlgebra.Defs
GeneralizedBooleanAlgebra.toDistribLattice : {α : Type u} → [self : GeneralizedBooleanAlgebra α] → DistribLattice α
-- Mathlib.RingTheory.Trace.Basic
trace_eq_sum_embeddings_gen : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (E : Type u_7)
  [inst_3 : Field E] [inst_4 : Algebra K E] (pb : PowerBasis K L),
  (Polynomial.map (algebraMap K E) (minpoly K pb.gen)).Splits →
    IsSeparable K pb.gen → (algebraMap K E) ((Algebra.trace K L) pb.gen) = ∑ σ, σ pb.gen
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.throw_Option : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α : Type} {e : PUnit.{1}}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.except PUnit.{1} Std.Do.PostShape.pure)} [inst : Monad m]
  [Std.Do.WPMonad m ps], ⦃Q.2.1 e⦄ MonadExceptOf.throw e ⦃Q⦄
-- Mathlib.Analysis.Calculus.TangentCone.Basic
/-- **Alias** of the forward direction of `uniqueDiffWithinAt_closure`. -/
UniqueDiffWithinAt.of_closure : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {x : E} {s : Set E} [ContinuousAdd E] [ContinuousConstSMul 𝕜 E],
  UniqueDiffWithinAt 𝕜 (closure s) x → UniqueDiffWithinAt 𝕜 s x
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.whiskerLeft_toNatTrans : ∀ {C D E : CategoryTheory.Cat} (F : C ⟶ D) {G H : D ⟶ E} (η : G ⟶ H),
  (CategoryTheory.Bicategory.whiskerLeft F η).toNatTrans = F.toFunctor.whiskerLeft η.toNatTrans
-- Mathlib.Tactic.NormNum.RealSqrt
/-- `norm_num` extension that evaluates the function `Real.sqrt`.  -/
Mathlib.Meta.NormNum.evalRealSqrt : Mathlib.Meta.NormNum.NormNumExt
-- Aesop.RuleSet.Member
Aesop.instInhabitedBaseRuleSetMember.default : Aesop.BaseRuleSetMember
-- Mathlib.NumberTheory.DiophantineApproximation.Basic
_private.Mathlib.NumberTheory.DiophantineApproximation.Basic.0.Real.aux₁ : ∀ {ξ : ℝ} {u v : ℤ}, 2 ≤ v → Real.ContfracLegendre.Ass ξ u v → 0 < Int.fract ξ
-- Init.Data.SInt.Bitwise
Int16.zero_shiftLeft : ∀ {a : Int16}, 0 <<< a = 0
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.Result.config : Lean.Meta.Grind.Result → Lean.Grind.Config
-- Init.Control.Lawful.Instances
StateT.ext_iff : ∀ {σ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} {x y : StateT σ m α}, x = y ↔ ∀ (s : σ), x.run s = y.run s
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_congr : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited β] {a b : α}, (a == b) = true → m[a]! = m[b]!
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.sum_rpow_le_norm_rpow : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)],
  0 < p.toReal → ∀ (f : ↥(lp E p)) (s : Finset α), ∑ i ∈ s, ‖↑f i‖ ^ p.toReal ≤ ‖f‖ ^ p.toReal
-- Mathlib.Data.Finmap
Finmap.erase_toFinmap : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (s : AList β),
  Finmap.erase a s.toFinmap = (AList.erase a s).toFinmap
-- Mathlib.Order.Filter.Extr
IsExtrOn.comp_antitone : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {s : Set α} {a : α},
  IsExtrOn f s a → ∀ {g : β → γ}, Antitone g → IsExtrOn (g ∘ f) s a
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
/-- For a ring `R` and two modules `M` and `N`, a perfect pairing is a bilinear map `M × N → R`
that is bijective in both arguments.  -/
LinearMap.IsPerfPair : {R : Type u_1} →
  {M : Type u_3} →
    {N : Type u_5} →
      [inst : AddCommGroup M] →
        [inst_1 : AddCommGroup N] →
          [inst_2 : CommRing R] → [inst_3 : Module R M] → [inst_4 : Module R N] → (M →ₗ[R] N →ₗ[R] R) → Prop
-- Mathlib.LinearAlgebra.Span.Defs
Module.isPrincipal_def : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Module.IsPrincipal R M ↔ ⊤.IsPrincipal
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.eq_one_of_monic_natDegree_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.Monic → p.natDegree = 0 → p = 1
-- Mathlib.Tactic.Conv
/-- `with_reducible tacs` executes `tacs` using the reducible transparency setting.
In this setting only definitions tagged as `[reducible]` are unfolded.
 -/
Mathlib.Tactic.Conv.withReducible : Lean.ParserDescr
-- Init.Data.UInt.Bitwise
UInt8.ofFin_shiftLeft_mod : ∀ (a b : Fin UInt8.size), UInt8.ofFin (a <<< (b % 8)) = UInt8.ofFin a <<< UInt8.ofFin b
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelp : Type
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.instOneHom.eq_1 : ∀ (G H : GrpCat), G.instOneHom H = { one := GrpCat.ofHom 1 }
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
DifferentiableAt.ccos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E},
  DifferentiableAt ℂ f x → DifferentiableAt ℂ (fun x => Complex.cos (f x)) x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.bijOn_cos : Set.BijOn Real.cos (Set.Icc 0 Real.pi) (Set.Icc (-1) 1)
-- Init.Data.Nat.ToString
Nat.length_toDigits_le_iff : ∀ {b n k : ℕ}, 1 < b → 0 < k → ((b.toDigits n).length ≤ k ↔ n < b ^ k)
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {X : C} {arrows : CategoryTheory.Presieve X}
  {downward_closed : ∀ {Y Z : C} {f : Y ⟶ X}, arrows f → ∀ (g : Z ⟶ Y), arrows (CategoryTheory.CategoryStruct.comp g f)}
  {arrows_1 : CategoryTheory.Presieve X}
  {downward_closed_1 :
    ∀ {Y Z : C} {f : Y ⟶ X}, arrows_1 f → ∀ (g : Z ⟶ Y), arrows_1 (CategoryTheory.CategoryStruct.comp g f)},
  { arrows := arrows, downward_closed := downward_closed } =
      { arrows := arrows_1, downward_closed := downward_closed_1 } →
    arrows = arrows_1
-- Mathlib.Data.Multiset.ZeroCons
Multiset.card_eq_one : ∀ {α : Type u_1} {s : Multiset α}, s.card = 1 ↔ ∃ a, s = {a}
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.Descr : Type → Type → Type → Type
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.toReal_rnDeriv_tilted_left : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) {f : α → ℝ} {ν : MeasureTheory.Measure α}
  [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν],
  AEMeasurable f ν →
    (fun x => ((μ.tilted f).rnDeriv ν x).toReal) =ᵐ[ν] fun x =>
      (Real.exp (f x) / ∫ (x : α), Real.exp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.zsmul_congr : ∀ {R : Type u_2} [inst : CommRing R] {b b' c : R} {a a' : ℤ}, a = a' → b = b' → a' • b' = c → a • b = c
-- Init.Grind.AC
Lean.Grind.AC.instInhabitedSeq : Inhabited Lean.Grind.AC.Seq
-- Mathlib.Order.Category.CompleteLat
CompleteLat.of.inj : ∀ {carrier : Type u_1} {str : CompleteLattice carrier} {carrier_1 : Type u_1} {str_1 : CompleteLattice carrier_1},
  { carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 } → carrier = carrier_1 ∧ str ≍ str_1
-- Mathlib.LinearAlgebra.Ray
exists_pos_left_iff_sameRay_and_ne_zero : ∀ {R : Type u_1} [inst : Field R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {x y : M}, x ≠ 0 → ((∃ r, 0 < r ∧ r • x = y) ↔ SameRay R x y ∧ y ≠ 0)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_insertIfNew : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {k a fallback : α} {v : β},
      (m.insertIfNew k v).getKeyD a fallback = if (k == a) = true ∧ k ∉ m then k else m.getKeyD a fallback
-- Mathlib.Algebra.Category.MonCat.Basic
/-- The underlying type.  -/
AddCommMonCat.carrier : AddCommMonCat → Type u
-- Mathlib.Topology.Sets.Order
ClopenUpperSet.coe_sup : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LE α] (s t : ClopenUpperSet α), ↑(s ⊔ t) = ↑s ∪ ↑t
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → γ a} {k : α} [inst_1 : Inhabited (γ k)],
  (Std.DTreeMap.map f t).get! k = (Option.map (f k) (t.get? k)).get!
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.ι_mapBifunctorComp₁₂MapObjIso_hom_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9}
  {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r)
  (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂)
  (X₃ : CategoryTheory.GradedObject I₃ C₃)
  [inst_5 : (((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
              (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
          X₃).HasMap
      ρ₁₂.q]
  [H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃]
  [inst_7 :
    ((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj
          X₃).HasMap
      r]
  (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) {Z : C₄}
  (h_1 :
    CategoryTheory.GradedObject.mapBifunctorMapObj G ρ₁₂.q
        (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.ιMapTrifunctorMapObj (CategoryTheory.bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.GradedObject.mapBifunctorComp₁₂MapObjIso F₁₂ G ρ₁₂ X₁ X₂ X₃).hom j) h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) h_1
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.performRatCheck.eq_1 : ∀ {n : ℕ} (negPivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))
  (clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)))
  (rupUnits ratUnits : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)))
  (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (id : ℕ) (rupHints : Array ℕ),
  { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments }.performRatCheck
      negPivot (id, rupHints) =
    match clauses[id]! with
    | some c =>
      have negC := (c.delete negPivot).negate;
      match
        { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments }.insertRatUnits
          negC with
      | (f, foundContradiction) =>
        if foundContradiction = true then
          have f := f.clearRatUnits;
          (f, true)
        else
          match f.performRupCheck rupHints with
          | (f, derivedLits, derivedEmpty, encounteredError) =>
            match f with
            | { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments } =>
              have assignments :=
                Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.restoreAssignments assignments derivedLits;
              have f :=
                { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits,
                    assignments := assignments }.clearRatUnits;
              if (encounteredError || !derivedEmpty) = true then (f, false) else (f, true)
    | none => ({ clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments }, false)
-- Mathlib.Data.ZMod.Basic
ZMod.cast_injective_of_le : ∀ {m n : ℕ} [nzm : NeZero m], m ≤ n → Function.Injective ZMod.cast
-- Mathlib.NumberTheory.Padics.PadicVal.Defs
/-- A simplification of `padicValNat` when one input is prime, by analogy with
`padicValRat_def`.  -/
padicValNat_eq_emultiplicity : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ}, n ≠ 0 → ↑(padicValNat p n) = emultiplicity p n
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.recZeroCoe_one : ∀ {M : Type u_4} {N : Type u_5} [inst : One M] (f : M → N) (z : N), WithZero.recZeroCoe z f 1 = f 1
-- Mathlib.Order.PropInstances
Pi.instSymmBotForallForallProp : ∀ (α : Type u_4), Std.Symm ⊥
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k} {fallback : α},
  (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.minKeyD fallback =
    t.minKey?.elim k fun k' => if (compare k k').isLE = true then k else k'
-- Mathlib.Data.Nat.Prime.Defs
Nat.Prime.ne_one : ∀ {p : ℕ}, Nat.Prime p → p ≠ 1
-- Mathlib.MeasureTheory.Measure.Complex
MeasureTheory.ComplexMeasure.equivSignedMeasure_symm_apply : ∀ {α : Type u_1} {m : MeasurableSpace α} (x : MeasureTheory.SignedMeasure α × MeasureTheory.SignedMeasure α),
  MeasureTheory.ComplexMeasure.equivSignedMeasure.symm x =
    match x with
    | (s, t) => s.toComplexMeasure t
-- Mathlib.FieldTheory.RatFunc.Valuation
RatFunc.inftyValuationDef.congr_simp : ∀ (F : Type u_1) [inst : Field F] {inst_1 : DecidableEq (RatFunc F)} [inst_2 : DecidableEq (RatFunc F)]
  (r r_1 : RatFunc F), r = r_1 → RatFunc.inftyValuationDef F r = RatFunc.inftyValuationDef F r_1
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.IsNat.to_raw_eq : ∀ {α : Type u} {a : α} {n : ℕ} [inst : AddMonoidWithOne α], Mathlib.Meta.NormNum.IsNat a n → a = n.rawCast
-- Mathlib.Topology.ContinuousMap.Ideals
/-- The open set `ContinuousMap.setOfIdeal I` realized as a term of `opens X`.  -/
ContinuousMap.opensOfIdeal : {X : Type u_1} →
  {R : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : Semiring R] →
        [inst_2 : TopologicalSpace R] →
          [inst_3 : IsTopologicalSemiring R] → [T2Space R] → Ideal C(X, R) → TopologicalSpace.Opens X
-- Mathlib.AlgebraicTopology.TopologicalSimplex
SimplexCategory.toTop_map : ∀ {X Y : SimplexCategory} (f : X ⟶ Y),
  SimplexCategory.toTop.{u}.map f =
    TopCat.uliftFunctor.map
      (TopCat.ofHom { toFun := stdSimplex.map ⇑(CategoryTheory.ConcreteCategory.hom f), continuous_toFun := ⋯ })
-- Mathlib.Dynamics.Ergodic.Action.Regular
instErgodicVAddOfIsAddLeftInvariant : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [MeasurableAdd₂ G] [MeasurableNeg G]
  {μ : MeasureTheory.Measure G} [MeasureTheory.SFinite μ] [μ.IsAddLeftInvariant], ErgodicVAdd G G μ
-- Mathlib.CategoryTheory.Center.Linear
CategoryTheory.Linear.toCatCenter_apply_app : ∀ (R : Type w) [inst : Ring R] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] (a : R) (X : C),
  ((CategoryTheory.Linear.toCatCenter R C) a).app X = a • CategoryTheory.CategoryStruct.id X
-- Mathlib.Order.CompleteBooleanAlgebra
/-- Structure containing the minimal axioms required to check that an order is a coframe. Do NOT
use, except for implementing `Order.Coframe` via `Order.Coframe.ofMinimalAxioms`.

This structure omits the `sdiff`, `hnot` fields, which can be recovered using
`Order.Coframe.ofMinimalAxioms`.  -/
Order.Coframe.MinimalAxioms : (α : Type u) → [CompleteLattice α] → Prop
-- Mathlib.Geometry.Manifold.Diffeomorph
ModelWithCorners.extChartAt_transContinuousLinearEquiv_target : ∀ {𝕜 : 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_5}
  [inst_5 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_9} [inst_6 : TopologicalSpace M]
  [inst_7 : ChartedSpace H M] (e : E ≃L[𝕜] E') (x : M),
  (extChartAt (I.transContinuousLinearEquiv e) x).target = ⇑e.symm ⁻¹' (extChartAt I x).target
-- Mathlib.Data.List.Perm.Basic
List.perm_comp_perm : ∀ {α : Type u_1}, Relation.Comp List.Perm List.Perm = List.Perm
-- Mathlib.Topology.DiscreteQuotient
/-- When `X` is a locally connected space, there is an `OrderBot` instance on
`DiscreteQuotient X`. The bottom element is given by `connectedComponentSetoid X`
 -/
DiscreteQuotient.instOrderBotOfLocallyConnectedSpace : {X : Type u_2} → [inst : TopologicalSpace X] → [LocallyConnectedSpace X] → OrderBot (DiscreteQuotient X)
-- Mathlib.ModelTheory.Fraisse
/-- A structure `M` is ultrahomogeneous if every embedding of a finitely generated substructure
into `M` extends to an automorphism of `M`.  -/
FirstOrder.Language.IsUltrahomogeneous : (L : FirstOrder.Language) → (M : Type w) → [L.Structure M] → Prop
-- Init.Data.Int.Linear
Int.Internal.Linear.unsatEqDivCoeffCert : Int.Internal.Linear.Expr → Int.Internal.Linear.Expr → ℤ → Bool
-- Lean.Parser.Types
_private.Lean.Parser.Types.0.Lean.Parser.SyntaxStack.mk.sizeOf_spec : ∀ (raw : Array Lean.Syntax) (drop : ℕ), sizeOf { raw := raw, drop := drop } = 1 + sizeOf raw + sizeOf drop
-- Mathlib.Order.Atoms
GaloisInsertion.isAtom_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : PartialOrder β] [inst_2 : OrderBot α] [IsAtomic α]
  [inst_4 : OrderBot β] {l : α → β} {u : β → α} (gi : GaloisInsertion l u),
  u ⊥ = ⊥ → (∀ (a : α), IsAtom a → u (l a) = a) → ∀ (a : α), IsAtom (l a) ↔ IsAtom a