mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.swapLeft_zero : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ}, ProbabilityTheory.Kernel.swapLeft 0 = 0
-- Mathlib.Tactic.NormNum.Core
/-- Run each registered `norm_num` extension on a typed expression `p : Prop`,
and returning the truth or falsity of `p' : Prop` from an equivalence `p ↔ p'`.  -/
Mathlib.Meta.NormNum.deriveBool : (p : Q(Prop)) → Lean.MetaM ((b : Bool) × Mathlib.Meta.NormNum.BoolResult p b)
-- Mathlib.Order.Filter.ZeroAndBoundedAtFilter
/-- `zeroAtFilterSubmodule l` is the submodule of `f : α → β` which
tend to zero along `l`.  -/
Filter.zeroAtFilterSubmodule : (𝕜 : Type u_1) →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : TopologicalSpace β] →
        [inst_1 : Semiring 𝕜] →
          [inst_2 : AddCommMonoid β] →
            [inst_3 : Module 𝕜 β] → [ContinuousAdd β] → [ContinuousConstSMul 𝕜 β] → Filter α → Submodule 𝕜 (α → β)
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.le_op_iff : ∀ {M : Type u_2} [inst : Add M] {S₁ : AddSubsemigroup Mᵃᵒᵖ} {S₂ : AddSubsemigroup M}, S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂
-- Mathlib.Topology.MetricSpace.Thickening
Metric.mem_thickening_iff_exists_edist_lt : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ} (E : Set α) (x : α),
  x ∈ Metric.thickening δ E ↔ ∃ z ∈ E, edist x z < ENNReal.ofReal δ
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instZeroOfAddOpposite : {M : Type u_1} → [Zero Mᵃᵒᵖ] → Zero Mᵈᵃᵃ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.ofList_eq_insertMany_empty : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {l : List (α × β)},
  Std.DTreeMap.Const.ofList l cmp = Std.DTreeMap.Const.insertMany ∅ l
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.trW_iff' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [P.IsStableUnderShift ℤ] {Y Z : C} (g : Y ⟶ Z),
  P.trW g ↔
    ∃ X f h,
      ∃ (_ : CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles),
        P X
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzWith.lipschitzOnWith : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β}
  {s : Set α}, LipschitzWith K f → LipschitzOnWith K f s
-- Mathlib.Data.Multiset.Count
Multiset.countP_le_of_le : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] {s t : Multiset α},
  s ≤ t → Multiset.countP p s ≤ Multiset.countP p t
-- Mathlib.Order.CompleteLattice.Basic
iSup_eq_bot : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {s : ι → α}, iSup s = ⊥ ↔ ∀ (i : ι), s i = ⊥
-- Mathlib.Logic.Relation
/-- **Alias** of `Relation.reflTransGen_le_of_equivalence_of_le`. -/
Relation.reflTransGen_of_equivalence : ∀ {α : Type u_1} {r r' : α → α → Prop}, Equivalence r → r' ≤ r → Relation.ReflTransGen r' ≤ r
-- Batteries.Data.List.Lemmas
List.dropLast_eq_eraseIdx : ∀ {α : Type u_1} {xs : List α} {i : ℕ}, i + 1 = xs.length → xs.dropLast = xs.eraseIdx i
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedAction : Inhabited Lean.Meta.Grind.Action
-- Init.Data.List.Impl
List.findSomeRev?.eq_def : ∀ {α : Type u} {β : Type v} (f : α → Option β) (x : List α),
  List.findSomeRev? f x =
    match x with
    | [] => none
    | a :: as =>
      match List.findSomeRev? f as with
      | some b => some b
      | none => f a
-- Lean.Environment
/-- Trie of declaration names without private name prefixes for fast longest-prefix access.  -/
_private.Lean.Environment.0.Lean.AsyncConsts.normalizedTrie : Lean.AsyncConsts✝ → Lean.NameTrie Lean.AsyncConst✝
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.CWComplex.Subcomplex.coe_mk'' : ∀ {X : Type u_1} [t : TopologicalSpace X] [inst : T2Space X] (C : Set X) [h : Topology.CWComplex C] (E : Set X)
  (I : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) [inst_1 : Topology.CWComplex E]
  (union : ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = E), ↑(Topology.CWComplex.Subcomplex.mk'' C E I union) = E
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal.0.AugmentedSimplexCategory.tensorObj.match_1.eq_1 : ∀ (motive : AugmentedSimplexCategory → AugmentedSimplexCategory → Sort u_1) (m n : SimplexCategory)
  (h_1 : (m n : SimplexCategory) → motive (CategoryTheory.WithInitial.of m) (CategoryTheory.WithInitial.of n))
  (h_2 : (x : AugmentedSimplexCategory) → motive CategoryTheory.WithInitial.star x)
  (h_3 : (x : AugmentedSimplexCategory) → motive x CategoryTheory.WithInitial.star),
  (match CategoryTheory.WithInitial.of m, CategoryTheory.WithInitial.of n with
    | CategoryTheory.WithInitial.of m, CategoryTheory.WithInitial.of n => h_1 m n
    | CategoryTheory.WithInitial.star, x => h_2 x
    | x, CategoryTheory.WithInitial.star => h_3 x) =
    h_1 m n
-- Init.Data.Int.DivMod.Lemmas
Int.mul_fmod_left : ∀ (a b : ℤ), (a * b).fmod b = 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.variableChange_j : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R)
  [inst_1 : W.IsElliptic], (C • W).j = W.j
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.lift_max : ∀ {a b : Cardinal.{v}}, Cardinal.lift.{u, v} (max a b) = max (Cardinal.lift.{u, v} a) (Cardinal.lift.{u, v} b)
-- Mathlib.CategoryTheory.Sites.SheafHom
/-- Given two presheaves `F` and `G` on a category `C` with values in a category `A`,
this `presheafHom F G` is the presheaf of types which sends an object `X : C`
to the type of morphisms between the "restrictions" of `F` and `G` to the category `Over X`.  -/
CategoryTheory.presheafHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} A] →
        CategoryTheory.Functor Cᵒᵖ A →
          CategoryTheory.Functor Cᵒᵖ A → CategoryTheory.Functor Cᵒᵖ (Type (max (max u v) v'))
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.im_natCast : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : AddCommGroupWithOne R] (n : ℕ), (↑n).im = 0
-- Init.Data.Array.Lemmas
Array.filter_replicate_of_neg : ∀ {stop n : ℕ} {α : Type u_1} {p : α → Bool} {a : α},
  stop = n → ¬p a = true → Array.filter p (Array.replicate n a) 0 stop = #[]
-- Mathlib.Algebra.Lie.Basic
/-- The inverse function of an equivalence of Lie algebras  -/
LieEquiv.invFun : {R : Type u} →
  {L : Type v} →
    {L' : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] → [inst_3 : LieRing L'] → [inst_4 : LieAlgebra R L'] → (L ≃ₗ⁅R⁆ L') → L' → L
-- Mathlib.Topology.UniformSpace.Closeds
UniformContinuous.sup_compacts : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β]
  {f g : α → TopologicalSpace.Compacts β},
  UniformContinuous f → UniformContinuous g → UniformContinuous fun x => f x ⊔ g x
-- Mathlib.Tactic.Simproc.VecPerm
/-- The `vecPerm` simproc computes the new entries of a vector after applying a permutation to them.
This can be used to simplify expressions as follows:
```
example {a b c : Nat} : ![a, b, c] ∘ Equiv.swap 0 1 = ![b, a, c] := by
  simp [vecPerm, Equiv.swap_apply_def]
```
Note that for this simproc to work, dsimp needs to be able to simplify the individual applications
of the permutation.
 -/
Mathlib.Tactic.FinVec.vecPerm : Lean.Meta.Simp.Simproc
-- Mathlib.Order.RelClasses
/-- Set notation form of `le_of_le_of_eq` -/
subset_of_subset_of_eq : ∀ {α : Type u_1} [UsesSetNotationForOrder α] {a b c : α} [inst : LE α], a ⊆ b → b = c → a ⊆ c
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_add_intCast_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℤ), toIcoDiv hp a (b + ↑m * p) = toIcoDiv hp a b + m
-- Mathlib.Data.Set.Lattice
Set.biInter_subset_biUnion : ∀ {α : Type u_1} {β : Type u_2} {s : Set α}, s.Nonempty → ∀ {t : α → Set β}, ⋂ x ∈ s, t x ⊆ ⋃ x ∈ s, t x
-- Mathlib.CategoryTheory.Limits.Yoneda
CategoryTheory.Coyoneda.colimitCocone_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : Cᵒᵖ),
  (CategoryTheory.Coyoneda.colimitCocone X).pt = PUnit.{v + 1}
-- Init.Internal.Order.Lemmas
Lean.Order.Array.monotone_allM : ∀ {γ : Type w} [inst : Lean.Order.PartialOrder γ] {m : Type → Type v} [inst_1 : Monad m]
  [inst_2 : (α : Type) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m] {α : Type u} (f : γ → α → m Bool)
  (xs : Array α) (start stop : ℕ), Lean.Order.monotone f → Lean.Order.monotone fun x => Array.allM (f x) xs start stop
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
/-- A copy of a complete equipartite graph identifies a complete equipartite subgraph.  -/
SimpleGraph.CompleteEquipartiteSubgraph.ofCopy : {V : Type u_1} →
  {G : SimpleGraph V} →
    {r t : ℕ} → (SimpleGraph.completeEquipartiteGraph r t).Copy G → G.CompleteEquipartiteSubgraph r t
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Neg
Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastNeg : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (value : BitVec w)
  (target : aig.RefVec w) (assign : α → Bool),
  (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := target.get idx hidx }⟧ = value.getLsbD idx) →
    ∀ (idx : ℕ) (hidx : idx < w),
      ⟦assign,
          { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastNeg aig target).aig,
            ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastNeg aig target).vec.get idx hidx }⟧ =
        (-value).getLsbD idx
-- Init.Data.SInt.Lemmas
Int8.neg_neg : ∀ {a : Int8}, - -a = a
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- Build an isomorphism in the category `MagmaCat` from a `MulEquiv` between `Mul`s.  -/
MulEquiv.toMagmaCatIso : {X Y : Type u} → [inst : Mul X] → [inst_1 : Mul Y] → X ≃* Y → (MagmaCat.of X ≅ MagmaCat.of Y)
-- Mathlib.Probability.Distributions.Binomial
ProbabilityTheory.binomial_nat : ∀ {n : ℕ} {p : ↑unitInterval},
  MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.binomial n p) = ProbabilityTheory.binomial n p
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.le_log_of_exp_le : ∀ {G : Type u_3} [inst : Preorder G] {a : G} [inst_1 : AddGroup G] {x : WithZero (Multiplicative G)},
  WithZero.exp a ≤ x → a ≤ x.log
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.ValueGroupWithZero.lift_valuation : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : ValuativeRel R] {α : Sort u_3} (f : R → ↥(ValuativeRel.posSubmonoid R) → α)
  (hf : ∀ (x y : R) (t s : ↥(ValuativeRel.posSubmonoid R)), x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → f x s = f y t)
  (x : R), ValuativeRel.ValueGroupWithZero.lift f hf ((ValuativeRel.valuation R) x) = f x 1
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.Slice.endsWith_string_iff : ∀ {pat : String} {s : String.Slice}, s.endsWith pat = true ↔ pat.toList <:+ s.copy.toList
-- Mathlib.Algebra.Algebra.Unitization
Unitization.inl_zero : ∀ {R : Type u_3} (A : Type u_4) [inst : Zero R] [inst_1 : Zero A], Unitization.inl 0 = 0
-- Init.Data.Iterators.Basic
/-- If present, applies `f` to the iterator of an `IterStep` and replaces the iterator
with the result of the application of `f`.
 -/
Std.IterStep.mapIterator : {α : Type u} → {β : Type w} → {α' : Type u'} → (α → α') → Std.IterStep α β → Std.IterStep α' β
-- Init.Data.List.TakeDrop
List.takeWhile_append_dropWhile : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.takeWhile p l ++ List.dropWhile p l = l
-- Mathlib.CategoryTheory.Widesubcategory
/-- Structure for wide subcategories. Objects ignore the morphism property.
 -/
CategoryTheory.WideSubcategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (_P : CategoryTheory.MorphismProperty C) → [_P.IsMultiplicative] → Type u₁
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.ppPattern : Lean.Expr → Lean.MessageData
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.rcons.eq_1 : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [inst_2 : DecidableEq ι]
  [inst_3 : (i : ι) → DecidableEq (G i)] (i : ι) (p : Monoid.PushoutI.NormalWord.Pair d i),
  Monoid.PushoutI.NormalWord.rcons i p =
    {
      toWord :=
        (Monoid.CoprodI.Word.equivPair i).symm
          (let __src := p.toPair;
          { head := ↑(⋯.equiv p.head).2, tail := __src.tail, fstIdx_ne := ⋯ }),
      head := (MonoidHom.ofInjective ⋯).symm (⋯.equiv p.head).1, normalized := ⋯ }
-- Mathlib.Tactic.FBinop
/-- Try to coerce elements in the tree to `maxS` when needed.  -/
_private.Mathlib.Tactic.FBinop.0.FBinopElab.applyCoe : FBinopElab.Tree✝ → FBinopElab.SRec → Lean.Elab.TermElabM FBinopElab.Tree✝
-- Mathlib.Order.MinMax
max_le_max_left : ∀ {α : Type u} [inst : LinearOrder α] {a b : α} (c : α), a ≤ b → max c a ≤ max c b
-- Mathlib.Algebra.Group.Submonoid.BigOperators
/-- Product of elements of a submonoid of a `CommMonoid` indexed by a `Finset` is in the
submonoid.  -/
Submonoid.prod_mem : ∀ {M : Type u_4} [inst : CommMonoid M] (S : Submonoid M) {ι : Type u_5} {t : Finset ι} {f : ι → M},
  (∀ c ∈ t, f c ∈ S) → ∏ c ∈ t, f c ∈ S
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosSemidef.diagonal : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  [inst_4 : DecidableEq n] {d : n → R}, 0 ≤ d → (Matrix.diagonal d).PosSemidef
-- Init.Data.List.Lemmas
List.map_reverse : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α}, List.map f l.reverse = (List.map f l).reverse
-- Mathlib.FieldTheory.Relrank
Subfield.relfinrank_map_map : ∀ {E : Type v} [inst : Field E] {L : Type w} [inst_1 : Field L] (A B : Subfield E) (f : E →+* L),
  (Subfield.map f A).relfinrank (Subfield.map f B) = A.relfinrank B
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.evalAlts.goWithIncremental : Lean.Meta.ElimInfo →
  Array Lean.Elab.Tactic.ElimApp.Alt →
    Lean.Syntax →
      Option (Array Lean.Syntax) →
        Lean.Syntax →
          ℕ →
            Array Lean.FVarId →
              Array Lean.FVarId →
                Array (Lean.Ident × Lean.FVarId) →
                  Array (Lean.Language.SnapshotBundle Lean.Elab.Tactic.TacticParsedSnapshot) →
                    Lean.Elab.Tactic.TacticM (List Lean.MVarId)
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.coe_disjoint : ∀ {α : Type u_2} [inst : TopologicalSpace α] {s t : TopologicalSpace.Opens α}, Disjoint ↑s ↑t ↔ Disjoint s t
-- Mathlib.Order.Monotone.Defs
antitone_const : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {c : β}, Antitone fun x => c
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.addHom_ext_iff : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {M : Type u_3} [inst_1 : AddZeroClass M]
  {f g : SkewMonoidAlgebra k G →+ M},
  f = g ↔ ∀ (a : G) (b : k), f (SkewMonoidAlgebra.single a b) = g (SkewMonoidAlgebra.single a b)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.ofDiseqSplit.sizeOf_spec : ∀ (c₁ : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr) (decVar : Lean.FVarId) (h : Lean.Meta.Grind.Arith.Cutsat.UnsatProof)
  (decVars : Array Lean.FVarId),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.ofDiseqSplit c₁ decVar h decVars) =
    1 + sizeOf c₁ + sizeOf decVar + sizeOf h + sizeOf decVars
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_flip : ∀ {M : Type u_4} [inst : CommMonoid M] {n : ℕ} (f : ℕ → M),
  ∏ r ∈ Finset.range (n + 1), f (n - r) = ∏ k ∈ Finset.range (n + 1), f k
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.shiftMap.eq_1 : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : F.ShiftSequence M] {X Y : C} {n : M}
  (f : X ⟶ (CategoryTheory.shiftFunctor C n).obj Y) (a a' : M) (ha' : n + a = a'),
  F.shiftMap f a a' ha' = CategoryTheory.CategoryStruct.comp ((F.shift a).map f) ((F.shiftIso n a a' ha').hom.app Y)
-- Mathlib.Algebra.DirectSum.Ring
/-- The canonical map from ℕ to a graded semiring respects successors.  -/
DirectSum.GSemiring.natCast_succ : ∀ {ι : Type u_1} {A : ι → Type u_2} {inst : AddMonoid ι} {inst_1 : (i : ι) → AddCommMonoid (A i)}
  [self : DirectSum.GSemiring A] (n : ℕ),
  DirectSum.GSemiring.natCast (n + 1) = DirectSum.GSemiring.natCast n + GradedMonoid.GOne.one
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.mul.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α], Finset.mul = { mul := Finset.image₂ fun x1 x2 => x1 * x2 }
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_hom_app_fst_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} B₁]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁}
  {X : Type u₇} {Y : Type u₈} [inst_6 : CategoryTheory.Category.{v₇, u₇} X]
  [inst_7 : CategoryTheory.Category.{v₈, u₈} Y] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁)
  (U : CategoryTheory.Functor X Y) (X_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y) (x : X),
  ((CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U)
                  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ)
                  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ)
                  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U)).hom.app
            X_1).fst.app
      x =
    CategoryTheory.CategoryStruct.id (ψ.left.obj (X_1.fst.obj (U.obj x)))
-- Init.Data.Option.Lemmas
_private.Init.Data.Option.Lemmas.0.Option.merge.match_1.eq_4 : ∀ {α : Type u_1} (motive : Option α → Option α → Sort u_2) (x y : α) (h_1 : Unit → motive none none)
  (h_2 : (x : α) → motive (some x) none) (h_3 : (y : α) → motive none (some y))
  (h_4 : (x y : α) → motive (some x) (some y)),
  (match some x, some y with
    | none, none => h_1 ()
    | some x, none => h_2 x
    | none, some y => h_3 y
    | some x, some y => h_4 x y) =
    h_4 x y
-- Mathlib.NumberTheory.PythagoreanTriples
PythagoreanTriple.mul_isClassified : ∀ {x y z : ℤ} (h : PythagoreanTriple x y z) (k : ℤ), h.IsClassified → ⋯.IsClassified
-- Mathlib.Order.Atoms
Pi.isAtom_iff : ∀ {ι : Type u_4} {π : ι → Type u} {f : (i : ι) → π i} [inst : (i : ι) → PartialOrder (π i)]
  [inst_1 : (i : ι) → OrderBot (π i)], IsAtom f ↔ ∃ i, IsAtom (f i) ∧ ∀ (j : ι), j ≠ i → f j = ⊥
-- Mathlib.Algebra.Group.ULift
ULift.leftCancelSemigroup.eq_1 : ∀ {α : Type u} [inst : LeftCancelSemigroup α],
  ULift.leftCancelSemigroup = Function.Injective.leftCancelSemigroup ⇑Equiv.ulift ⋯ ⋯
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom_aux : ∀ (R S : CommRingCat) (p : PrimeSpectrum ↑R) [inst : Algebra ↑R ↑S]
  (y :
    ↑(((TopCat.Presheaf.pushforward CommRingCat
                (AlgebraicGeometry.Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
            (AlgebraicGeometry.Spec.structureSheaf ↑S).obj).stalk
        p)),
  ∃ x, x.2 • y = (AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom R S p) x.1
-- Init.Data.UInt.Lemmas
UInt32.ne_of_toBitVec_ne : ∀ {a b : UInt32}, a.toBitVec ≠ b.toBitVec → a ≠ b
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
HasFPowerSeriesOnBall.differentiableOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {f : E → F} {x : E} [CompleteSpace F],
  HasFPowerSeriesOnBall f p x r → DifferentiableOn 𝕜 f (Metric.eball x r)
-- Mathlib.CategoryTheory.Bicategory.Basic
/-- Precomposition of a 1-morphism as a functor.  -/
CategoryTheory.Bicategory.precomp : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] → {a b : B} → (c : B) → (a ⟶ b) → CategoryTheory.Functor (b ⟶ c) (a ⟶ c)
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.padicNormE.image : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {q : ℚ_[p]}, q ≠ 0 → ∃ n, ‖q‖ = ↑(↑p ^ (-n))
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.isCompact_closure_of_mem_openRcNhds : ∀ {α : Type u_1} [inst : TopologicalSpace α] {K : TopologicalSpace.Compacts α} {U : TopologicalSpace.Opens α},
  U ∈ K.openRcNhds → IsCompact (closure ↑U)
-- Mathlib.Order.Basic
/-- monotonicity of `≤` with respect to `→`  -/
le_imp_le_of_le_of_le : ∀ {α : Type u_2} [inst : Preorder α] {a b c d : α}, c ≤ a → b ≤ d → a ≤ b → c ≤ d
-- Mathlib.Lean.Meta.RefinedDiscrTree.Encode
/-- Determine whether the argument should be ignored.  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Encode.0.Lean.Meta.RefinedDiscrTree.getStackEntries.isIgnoredArg : Lean.Expr → Lean.Expr → Lean.BinderInfo → Lean.MetaM Bool
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- Two morphisms `f : X ⟶ Y` and `g : X ⟶ Z` have a pushout if the diagram `span f g` has a
colimit.  -/
CategoryTheory.Limits.HasPushout : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y Z : C} → (X ⟶ Y) → (X ⟶ Z) → Prop
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.algebraMap_def : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : CommSemiring S] [inst_6 : Algebra S A]
  [inst_7 : SMulCommClass R S A],
  algebraMap S (TensorProduct R A B) = Algebra.TensorProduct.includeLeftRingHom.comp (algebraMap S A)
-- Mathlib.Tactic.TermCongr
/-- Ensures the expected type is an iff. Returns the iff.
This expression satisfies `Lean.Expr.iff?`.  -/
Mathlib.Tactic.TermCongr.mkIffForExpectedType : Option Lean.Expr → Lean.MetaM Lean.Expr
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayerTarget.w : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} → {outWidth : ℕ} → Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayerTarget aig outWidth → ℕ
-- Std.Http.Protocol.H1.Reader
/-- Count of messages that this connection has already parsed.
 -/
Std.Http.Protocol.H1.Reader.messageCount : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Reader dir → ℕ
-- Mathlib.Algebra.ContinuedFractions.TerminatedStable
_private.Mathlib.Algebra.ContinuedFractions.TerminatedStable.0.GenContFract.contsAux.match_1.splitter : {K : Type u_1} →
  (motive : Option (GenContFract.Pair K) → Sort u_2) →
    (x : Option (GenContFract.Pair K)) →
      (Unit → motive none) → ((gp : GenContFract.Pair K) → motive (some gp)) → motive x
-- Mathlib.CategoryTheory.Sites.Pretopology
/-- We have a Galois insertion from pretopologies to Grothendieck topologies.  -/
CategoryTheory.Pretopology.gi : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      GaloisInsertion CategoryTheory.Pretopology.toGrothendieck CategoryTheory.GrothendieckTopology.toPretopology
-- Std.Data.HashSet.Lemmas
Std.HashSet.filter_equiv_self_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {f : α → Bool},
  (Std.HashSet.filter f m).Equiv m ↔ ∀ (k : α) (h : k ∈ m), f (m.get k h) = true