mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.TFAE
/-- Attempt to prove a statement of the form `TFAE [P₁, P₂, ...]`.  -/
Mathlib.Tactic.TFAE.proveTFAE : Array (ℕ × ℕ × Lean.Expr) → Array Q(Prop) → List ℕ → (l : Q(List Prop)) → Lean.MetaM Q(«$l».TFAE)
-- Mathlib.Probability.Kernel.Composition.MeasureComp
MeasureTheory.Measure.map_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (μ : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α β) {f : β → γ},
  Measurable f → MeasureTheory.Measure.map f (μ.bind ⇑κ) = μ.bind ⇑(κ.map f)
-- Mathlib.Data.Set.Operations
Set.mem_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : Set ι} {t : (i : ι) → Set (α i)} {f : (i : ι) → α i},
  f ∈ s.pi t ↔ ∀ i ∈ s, f i ∈ t i
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- The action map is compatible with multiplication.  -/
CategoryTheory.ModObj.mul_smul : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D}
  {M : C} {inst_4 : CategoryTheory.MonObj M} (X : D) [self : CategoryTheory.ModObj M X],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft CategoryTheory.MonObj.mul X)
      CategoryTheory.ModObj.smul =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso M M X).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight M CategoryTheory.ModObj.smul)
        CategoryTheory.ModObj.smul)
-- Std.Do.PostCond
Std.Do.ExceptConds.imp_elim : ∀ {ps : Std.Do.PostShape} {P Q R : Std.Do.ExceptConds ps}, P.entails (Q →ₑ R) → (P ∧ₑ Q).entails R
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.comp_τ₃_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} (φ₁₂ : S₁ ⟶ S₂) (φ₂₃ : S₂ ⟶ S₃) {Z : C} (h : S₃.X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp φ₁₂ φ₂₃).τ₃ h =
    CategoryTheory.CategoryStruct.comp φ₁₂.τ₃ (CategoryTheory.CategoryStruct.comp φ₂₃.τ₃ h)
-- Mathlib.Data.Finset.Sym
Finset.sym_inter : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α) (n : ℕ), (s ∩ t).sym n = s.sym n ∩ t.sym n
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.codomain_trivial : ∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) [h : Subsingleton α],
  Subsingleton β
-- Mathlib.RingTheory.Localization.Cardinality
/-- If you do not localize at any zero-divisors, localization preserves cardinality.  -/
IsLocalization.cardinalMk : ∀ {R : Type u} [inst : CommRing R] (L : Type u) [inst_1 : CommRing L] [inst_2 : Algebra R L] (S : Submonoid R)
  [IsLocalization S L], S ≤ nonZeroDivisors R → Cardinal.mk L = Cardinal.mk R
-- Mathlib.CategoryTheory.Abelian.Refinements
CategoryTheory.ShortComplex.Exact.exact_up_to_refinements : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S : CategoryTheory.ShortComplex C},
  S.Exact →
    ∀ {A : C} (x₂ : A ⟶ S.X₂),
      CategoryTheory.CategoryStruct.comp x₂ S.g = 0 →
        ∃ A' π,
          ∃ (_ : CategoryTheory.Epi π),
            ∃ x₁, CategoryTheory.CategoryStruct.comp π x₂ = CategoryTheory.CategoryStruct.comp x₁ S.f
-- Mathlib.RingTheory.LinearDisjoint
/-- If `A` and `B` are `R`-algebras, such that there exists a domain `S` over `R`
such that `A` and `B` inject into it and their images are linearly disjoint,
then `A ⊗[R] B` is also a domain.  -/
Subalgebra.LinearDisjoint.isDomain_of_injective : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [IsDomain S]
  {A : Type u_1} {B : Type u_2} [inst_4 : Semiring A] [inst_5 : Semiring B] [inst_6 : Algebra R A]
  [inst_7 : Algebra R B] {fa : A →ₐ[R] S} {fb : B →ₐ[R] S},
  Function.Injective ⇑fa → Function.Injective ⇑fb → fa.range.LinearDisjoint fb.range → IsDomain (TensorProduct R A B)
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.delabCore : {α : Type} →
  Lean.Expr →
    optParam Lean.PrettyPrinter.Delaborator.OptionsPerPos ∅ →
      Lean.PrettyPrinter.Delaborator.DelabM α → Lean.MetaM (α × Lean.SubExpr.PosMap Lean.Elab.Info)
-- Init.Data.Int.Bitwise.Lemmas
Int.shiftLeft_shiftRight_eq : ∀ (a : ℤ) (b c : ℕ), a <<< b >>> c = a <<< (b - c) >>> (c - b)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_insertIfNew_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.insertIfNew k v).contains k = true
-- Mathlib.Algebra.Free
FreeAddMagma.map_of : ∀ {α : Type u} {β : Type v} (f : α → β) (x : α), (FreeAddMagma.map f) (FreeAddMagma.of x) = FreeAddMagma.of (f x)
-- Mathlib.Order.Basic
Prod.swap_le_swap : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] {x y : α × β}, x.swap ≤ y.swap ↔ x ≤ y
-- Mathlib.Analysis.Normed.Module.Completion
/-- Embedding of a normed space to its completion as a continuous linear map.  -/
UniformSpace.Completion.toComplL : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : Semiring 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] →
        [inst_2 : Module 𝕜 E] → [inst_3 : UniformContinuousConstSMul 𝕜 E] → E →L[𝕜] UniformSpace.Completion E
-- Std.Data.TreeSet.Basic
/-- Computes the difference of the given tree sets.

This function always iterates through the smaller set.
 -/
Std.TreeSet.diff : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp → Std.TreeSet α cmp → Std.TreeSet α cmp
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instAddMonoid.eq_1 : ∀ {α : Type u_1} [inst : AddMonoid α],
  OrderDual.instAddMonoid =
    { toAddSemigroup := OrderDual.instAddSemigroup, toZero := OrderDual.instZero, zero_add := ⋯, add_zero := ⋯,
      toNSMul := NSMul.ofSMul, nsmul_zero := ⋯, nsmul_succ := ⋯ }
-- Mathlib.RepresentationTheory.Homological.Resolution
/-- The hom of `k`-linear `G`-representations `k[G¹] → k` sending `∑ nᵢgᵢ ↦ ∑ nᵢ`.  -/
Rep.standardComplex.ε : (k G : Type u) → [inst : CommRing k] → [inst_1 : Monoid G] → Rep.ofMulAction k G (Fin 1 → G) ⟶ Rep.trivial k G k
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
uniqueDiffOn_extChartAt_target : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] (x : M), UniqueDiffOn 𝕜 (extChartAt I x).target
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.pairwise_disjoint_Ioc_add_intCast : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α] (a : α),
  Pairwise (Function.onFun Disjoint fun n => Set.Ioc (a + ↑n) (a + ↑n + 1))
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.contains.eq_1 : ∀ {n : ℕ} (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)
  (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)), c.contains l = List.contains c.clause l
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.decidableMemEdgeSet : {V : Type u} → (G : SimpleGraph V) → [DecidableRel G.Adj] → DecidablePred fun x => x ∈ G.edgeSet
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.refl : ∀ {M : Type u_1} [inst : Monoid M] (x : M), Associated x x
-- Mathlib.Order.Defs.LinearOrder
max_le : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, a ≤ c → b ≤ c → max a b ≤ c
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_15.eq_2 : ∀ (motive : Std.Tactic.BVDecide.BVUnOp → Sort u_1) (distance : ℕ) (h_1 : Unit → motive Std.Tactic.BVDecide.BVUnOp.not)
  (h_2 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateLeft distance))
  (h_3 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateRight distance))
  (h_4 : (distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst distance))
  (h_5 : Unit → motive Std.Tactic.BVDecide.BVUnOp.reverse) (h_6 : Unit → motive Std.Tactic.BVDecide.BVUnOp.clz)
  (h_7 : Unit → motive Std.Tactic.BVDecide.BVUnOp.cpop),
  (match Std.Tactic.BVDecide.BVUnOp.rotateLeft distance with
    | Std.Tactic.BVDecide.BVUnOp.not => h_1 ()
    | Std.Tactic.BVDecide.BVUnOp.rotateLeft distance => h_2 distance
    | Std.Tactic.BVDecide.BVUnOp.rotateRight distance => h_3 distance
    | Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst distance => h_4 distance
    | Std.Tactic.BVDecide.BVUnOp.reverse => h_5 ()
    | Std.Tactic.BVDecide.BVUnOp.clz => h_6 ()
    | Std.Tactic.BVDecide.BVUnOp.cpop => h_7 ()) =
    h_2 distance
-- Mathlib.Logic.Encodable.Basic
ULower.down.eq_1 : ∀ {α : Type u_1} [inst : Encodable α] (a : α), ULower.down a = (ULower.equiv α) a
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.sub_mem_comm_iff : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) {a b : G}, a - b ∈ H ↔ b - a ∈ H
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.solveElim : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr →
  Lean.Meta.Grind.Arith.Cutsat.DvdCnstr → Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.prod : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [h : ProbabilityTheory.IsZeroOrMarkovKernel κ]
  (η : ProbabilityTheory.Kernel α γ) [ProbabilityTheory.IsZeroOrMarkovKernel η],
  ProbabilityTheory.IsZeroOrMarkovKernel (κ.prod η)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- The `ComposableArrows C n` obtained by forgetting the first arrow.  -/
CategoryTheory.ComposableArrows.δ₀ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {n : ℕ} → CategoryTheory.ComposableArrows C (n + 1) → CategoryTheory.ComposableArrows C n
-- Std.Http.Protocol.H1
/-- Returns `true` when RFC semantics forbid a response payload body on the wire.
This includes informational responses, `204`, and `304`.

Reference: https://www.rfc-editor.org/rfc/rfc9112.html#name-message-body-length
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.responseMustNotHaveBody : Std.Http.Status → Bool
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.cgf_zero : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsZeroOrProbabilityMeasure μ], ProbabilityTheory.cgf X μ 0 = 0
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.instCompleteLattice : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C] →
      [CategoryTheory.WellPowered.{w, v₁, u₁} C] →
        [CategoryTheory.Limits.HasWidePullbacks C] →
          [CategoryTheory.Limits.HasImages C] →
            [CategoryTheory.Limits.HasCoproducts C] →
              [CategoryTheory.Limits.InitialMonoClass C] → {B : C} → CompleteLattice (CategoryTheory.Subobject B)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_id_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] {G H : CategoryTheory.OplaxFunctor B CategoryTheory.Cat}
  (θ : CategoryTheory.Oplax.StrongTrans G H) {a : B} {a' : CategoryTheory.Cat} (f : a' ⟶ G.obj a) (X : ↑a'),
  CategoryTheory.CategoryStruct.comp
      ((θ.naturality (CategoryTheory.CategoryStruct.id a)).hom.toNatTrans.app (f.toFunctor.obj X))
      ((H.mapId a).toNatTrans.app ((θ.app a).toFunctor.obj (f.toFunctor.obj X))) =
    (θ.app a).toFunctor.map ((G.mapId a).toNatTrans.app (f.toFunctor.obj X))
-- Mathlib.Analysis.Normed.Group.Quotient
/-- `S.normedMk` is surjective.  -/
AddSubgroup.surjective_normedMk : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] (S : AddSubgroup M), Function.Surjective ⇑S.normedMk
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_comp_toNNReal_comp : ∀ {ι : Type u_2} {f : ι → ENNReal}, (∀ (x : ι), f x ≠ ⊤) → (fun x => ↑x) ∘ ENNReal.toNNReal ∘ f = f
-- Mathlib.Topology.MetricSpace.Basic
AddOpposite.instMetricSpace : {α : Type u_2} → [MetricSpace α] → MetricSpace αᵃᵒᵖ
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.IsDynNetIn.of_le : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X} {m n : ℕ} {F s : Set X},
  m ≤ n → Dynamics.IsDynNetIn T F U m s → Dynamics.IsDynNetIn T F U n s
-- Init.Data.Array.Lemmas
Array.size_flatten : ∀ {α : Type u_1} {xss : Array (Array α)}, xss.flatten.size = (Array.map Array.size xss).sum
-- Init.Data.Array.Lemmas
Array.any_eq_true : ∀ {α : Type u_1} {p : α → Bool} {as : Array α}, as.any p = true ↔ ∃ i, ∃ (x : i < as.size), p as[i] = true
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Arrow.hasLimitsOfShape : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {T : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} T]
  [CategoryTheory.Limits.HasLimitsOfShape J T], CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.Arrow T)
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.instHashableOrigin : Hashable Lean.Meta.Origin
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.parseDayPeriodFrom : Std.Time.DayPeriodSymbols → Std.Internal.Parsec.String.Parser Std.Time.DayPeriod
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightId_inv_app_right : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  (L : CategoryTheory.Functor A T) (X : CategoryTheory.Comma L R),
  ((CategoryTheory.Comma.mapRightId R L).inv.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.LinearAlgebra.SpecialLinearGroup
/-- The coercion from `SpecialLinearGroup R V` to the function type `V → V`  -/
SpecialLinearGroup.instCoeFunForall : {R : Type u_1} →
  {V : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup V] → [inst_2 : Module R V] → CoeFun (SpecialLinearGroup R V) fun x => V → V
-- Mathlib.Algebra.Order.AddGroupWithTop
/-- In a `LinearOrderedAddCommMonoidWithTop`, the `⊤` element is invariant under addition.  -/
LinearOrderedAddCommMonoidWithTop.top_add' : ∀ {α : Type u_3} [self : LinearOrderedAddCommMonoidWithTop α] (x : α), ⊤ + x = ⊤
-- Mathlib.RingTheory.Polynomial.IsIntegral
Polynomial.isIntegral_coeff_of_factors : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Polynomial S),
  IsIntegral R p.leadingCoeff →
    p.Splits → (∀ (x : S), p.IsRoot x → IsIntegral R x) → ∀ (i : ℕ), IsIntegral R (p.coeff i)
-- Mathlib.Data.Set.Pairwise.Basic
/-- **Alias** of the reverse direction of `pairwise_subtype_iff_pairwise_set`. -/
Set.Pairwise.subtype : ∀ {α : Type u_1} (s : Set α) (r : α → α → Prop), s.Pairwise r → Pairwise fun x y => r ↑x ↑y
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.copy_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (f : A →A[R] B) (f' : A → B) (h : f' = ⇑f), f.copy f' h = f
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toArray_rio : ∀ {n i : ℕ}, (*...n).toArray[i]! = if i < n then i else 0
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.isImage_source_target : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), e.IsImage e.source e.target
-- Init.Data.String.Length
String.length_data : ∀ {b : String}, b.toList.length = b.length
-- Mathlib.CategoryTheory.Monoidal.Transport
CategoryTheory.Monoidal.transportStruct.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D),
  CategoryTheory.Monoidal.transportStruct e =
    {
      tensorObj := fun X Y =>
        e.functor.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj (e.inverse.obj X) (e.inverse.obj Y)),
      whiskerLeft := fun X x x_1 f =>
        e.functor.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (e.inverse.obj X) (e.inverse.map f)),
      whiskerRight := fun {X₁ X₂} f X =>
        e.functor.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight (e.inverse.map f) (e.inverse.obj X)),
      tensorHom := fun {X₁ Y₁ X₂ Y₂} f g =>
        e.functor.map (CategoryTheory.MonoidalCategoryStruct.tensorHom (e.inverse.map f) (e.inverse.map g)),
      tensorUnit := e.functor.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C),
      associator := fun X Y Z =>
        e.functor.mapIso
          (CategoryTheory.MonoidalCategory.whiskerRightIso
              (e.unitIso.app (CategoryTheory.MonoidalCategoryStruct.tensorObj (e.inverse.obj X) (e.inverse.obj Y))).symm
              (e.inverse.obj Z) ≪≫
            CategoryTheory.MonoidalCategoryStruct.associator (e.inverse.obj X) (e.inverse.obj Y) (e.inverse.obj Z) ≪≫
              CategoryTheory.MonoidalCategory.whiskerLeftIso (e.inverse.obj X)
                (e.unitIso.app (CategoryTheory.MonoidalCategoryStruct.tensorObj (e.inverse.obj Y) (e.inverse.obj Z)))),
      leftUnitor := fun X =>
        e.functor.mapIso
            (CategoryTheory.MonoidalCategory.whiskerRightIso
                (e.unitIso.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).symm (e.inverse.obj X) ≪≫
              CategoryTheory.MonoidalCategoryStruct.leftUnitor (e.inverse.obj X)) ≪≫
          e.counitIso.app X,
      rightUnitor := fun X =>
        e.functor.mapIso
            (CategoryTheory.MonoidalCategory.whiskerLeftIso (e.inverse.obj X)
                (e.unitIso.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).symm ≪≫
              CategoryTheory.MonoidalCategoryStruct.rightUnitor (e.inverse.obj X)) ≪≫
          e.counitIso.app X }
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool} {k fallback : α} (h : t.WF),
  (Std.DTreeMap.Raw.filter f t).getKeyD k fallback = ((t.getKey? k).pfilter fun x h' => f x (t.get x ⋯)).getD fallback
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Injective.injective_under : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.EnoughInjectives C] (X : C),
  CategoryTheory.Injective (CategoryTheory.Injective.under X)
-- Init.Data.Int.Gcd
Int.natAbs_le_lcm_right : ∀ {a : ℤ} (b : ℤ), a ≠ 0 → b.natAbs ≤ a.lcm b
-- Mathlib.Topology.Constructions
continuousAt_subtype_val : ∀ {X : Type u} [inst : TopologicalSpace X] {p : X → Prop} {x : Subtype p}, ContinuousAt Subtype.val x
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
SSet.Subcomplex.N.eq_iff_sMk_eq : ∀ {X : SSet} {A : X.Subcomplex} (x y : A.N),
  x = y ↔ { dim := x.dim, simplex := x.simplex } = { dim := y.dim, simplex := y.simplex }
-- Mathlib.Order.Defs.Unbundled
/-- **Alias** of `InvImage.irrefl`. -/
InvImage.irreflexive : ∀ {α : Sort u_1} {β : Sort u_2} (r : β → β → Prop) (f : α → β) [Std.Irrefl r], Std.Irrefl (InvImage r f)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.tr_respects : StateTransition.Respects Turing.ToPartrec.step (Turing.TM2.step Turing.PartrecToTM2.tr) Turing.PartrecToTM2.TrCfg
-- Mathlib.Data.EReal.Inv
EReal.mul_inv : ∀ (a b : EReal), (a * b)⁻¹ = a⁻¹ * b⁻¹
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.range_inl_sup_range_inr : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H],
  AddMonoid.Coprod.inl.range ⊔ AddMonoid.Coprod.inr.range = ⊤
-- Mathlib.MeasureTheory.Constructions.Cylinders
/-- A set `S` such that `t = cylinder s S`. `s` is given by `measurableCylinders.finset`.  -/
MeasureTheory.measurableCylinders.set : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : (i : ι) → MeasurableSpace (α i)] →
      {t : Set ((i : ι) → α i)} →
        (ht : t ∈ MeasureTheory.measurableCylinders α) →
          Set ((i : ↥(MeasureTheory.measurableCylinders.finset ht)) → α ↑i)
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.binaryProductTriangle_obj₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X₁ X₂ : C)
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasBinaryProduct X₁ X₂],
  (CategoryTheory.Pretriangulated.binaryProductTriangle X₁ X₂).obj₁ = X₁
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.embeddingUp'Add_f : ∀ {A : Type u_3} [inst : AddCommSemigroup A] [inst_1 : IsRightCancelAdd A] (a b x : A),
  (ComplexShape.embeddingUp'Add a b).f x = x + b
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.ι_toIso_inv : ∀ (X : AlgebraicGeometry.Scheme),
  CategoryTheory.CategoryStruct.comp ⊤.ι X.topIso.inv = CategoryTheory.CategoryStruct.id ↑⊤
-- Init.Data.Iterators.Combinators.FilterMap
/-- *Note: This is a very general combinator that requires an advanced understanding of monads,
dependent types and termination proofs. The variants `map` and `mapM` are easier to use and
sufficient for most use cases.*

If `it` is an iterator, then `it.mapWithPostcondition f` is another iterator that applies a monadic
function `f` to all values emitted by `it` and emits the result.

`f` is expected to return `PostconditionT n _`, where `n` is an arbitrary monad.
The `PostconditionT` transformer allows the caller to intrinsically prove properties about
`f`'s return value in the monad `n`, enabling termination proofs depending on the specific behavior
of `f`.

**Marble diagram (without monadic effects):**

```text
it                          ---a --b --c --d -e ----⊥
it.mapWithPostcondition     ---a'--b'--c'--d'-e'----⊥
```

(given that `f a = pure a'`, `f b = pure b'` etc.)

**Termination properties:**

* `Finite` instance: only if `it` is finite
* `Productive` instance: only if `it` is productive

For certain mapping functions `f`, the resulting iterator will be finite (or productive) even though
no `Finite` (or `Productive`) instance is provided. For example, if `f` is an `ExceptT` monad and
will always fail, then `it.mapWithPostcondition` will be finite even if `it` isn't.

In such situations, the missing instances can be proved manually if the postcondition bundled in
the `PostconditionT n` monad is strong enough. In the given example, a suitable postcondition might
be `fun _ => False`.

**Performance:**

For each value emitted by the base iterator `it`, this combinator calls `f`.
 -/
Std.Iter.mapWithPostcondition : {α β γ : Type w} →
  [Std.Iterator α Id β] →
    {m : Type w → Type w'} → [inst : Monad m] → (f : β → Std.Iterators.PostconditionT m γ) → Std.Iter β → Std.IterM m γ
-- Mathlib.Data.Erased
/-- Extracts the erased value, if it is a type.

Note: `(mk a).OutType` is not definitionally equal to `a`.
 -/
Erased.OutType : Erased (Sort u) → Sort u
-- Mathlib.Tactic.Algebra.Basic
/-- Handle scalar multiplication when the scalar ring `R'` doesn't match the base ring `R`.
Assumes `R` is an `R'`-algebra (i.e., `R'` is smaller), and casts the scalar using `algebraMap`.  -/
Mathlib.Tactic.Algebra.evalSMulCast : {u u' v : Lean.Level} →
  {R : Q(Type u)} →
    {R' : Q(Type u')} →
      {A : Q(Type v)} →
        {sR : Q(CommSemiring «$R»)} →
          {sA : Q(CommSemiring «$A»)} →
            (sAlg : Q(Algebra «$R» «$A»)) →
              (smul : Q(SMul «$R'» «$A»)) →
                (r' : Q(«$R'»)) → Lean.MetaM ((r : Q(«$R»)) × Q(∀ (a : «$A»), «$r» • a = «$r'» • a))