mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Array.Lemmas
Array.getElem_swapIfInBounds : ∀ {α : Type u_1} {xs : Array α} {i j k : ℕ} (hk : k < (xs.swapIfInBounds i j).size),
  (xs.swapIfInBounds i j)[k] =
    if h₁ : k = i ∧ j < xs.size then xs[j] else if h₂ : k = j ∧ i < xs.size then xs[i] else xs[k]
-- Lean.Meta.Sym.Apply
/-- A rule for backward chaining (goal transformation).

Given a goal `... ⊢ T`, applying a `BackwardRule` derived from a theorem `∀ xs, P`
will unify `T` with `P`, assign the goal to the theorem application,
and return new goals for the unassigned arguments in `xs`.
 -/
Lean.Meta.Sym.BackwardRule : Type
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_map : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {β : Type u_6} [inst_2 : MeasurableSpace β] {φ : α → β},
  AEMeasurable φ μ →
    ∀ {f : β → G},
      MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map φ μ) →
        ∫ (y : β), f y ∂MeasureTheory.Measure.map φ μ = ∫ (x : α), f (φ x) ∂μ
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
instLTMultiplicative : {α : Type u_1} → [LT α] → LT (Multiplicative α)
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.Splits.splits_rotateLeft : ∀ {s : String.Slice} {p : s.Pos} {t₁ t₂ t₃ : String} (h : p.Splits (t₁ ++ t₂) t₃), h.rotateLeft.Splits t₁ (t₂ ++ t₃)
-- Batteries.Data.List.Lemmas
List.pos_iff_exists_findIdxNth : ∀ {α : Type u_1} {i : ℕ} {p : α → Bool} {xs : List α} {h : i < xs.length},
  p xs[i] = true ↔ ∃ n, List.findIdxNth p xs n = i
-- Mathlib.Algebra.Order.Interval.Basic
instMulInterval.eq_1 : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : Mul α] [inst_2 : MulLeftMono α] [inst_3 : MulRightMono α],
  instMulInterval = { mul := WithBot.map₂ fun x1 x2 => x1 * x2 }
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_emptyc : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {a : α}, ∅[a]? = none
-- Mathlib.MeasureTheory.Measure.Doubling
IsUnifLocDoublingMeasure.mk : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] {μ : MeasureTheory.Measure α},
  (∃ C,
      ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0),
        ∀ (x : α), μ (Metric.closedBall x (2 * ε)) ≤ ↑C * μ (Metric.closedBall x ε)) →
    IsUnifLocDoublingMeasure μ
-- Mathlib.GroupTheory.PresentedGroup
PresentedGroup.mk_eq_one_iff : ∀ {α : Type u_1} {rels : Set (FreeGroup α)} {x : FreeGroup α},
  (PresentedGroup.mk rels) x = 1 ↔ x ∈ Subgroup.normalClosure rels
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.totallyDisconnectedSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y)
  [tdc : TotallyDisconnectedSpace X], TotallyDisconnectedSpace Y
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
MeasureTheory.Integrable.integral_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  {η : ProbabilityTheory.Kernel β γ} [inst_1 : NormedSpace ℝ E] ⦃f : γ → E⦄,
  MeasureTheory.Integrable f ((η.comp κ) a) → MeasureTheory.Integrable (fun x => ∫ (y : γ), f y ∂η x) (κ a)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.isLongestMatchAtChain_skipPrefixWhile : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  (s : String.Slice), String.Slice.Pattern.Model.IsLongestMatchAtChain pat s.startPos (s.skipPrefixWhile pat)
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.prod_target : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type w} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {E' : Type v'}
  [inst_4 : NormedAddCommGroup E'] [inst_5 : NormedSpace 𝕜 E'] {H' : Type w'} [inst_6 : TopologicalSpace H']
  (I' : ModelWithCorners 𝕜 E' H'), (I.prod I').target = (I.prod I'.toPartialEquiv).target
-- Mathlib.Data.List.Lex
_private.Mathlib.Data.List.Lex.0.List.Lex.isOrderConnected.aux : ∀ {α : Type u} (r : α → α → Prop) [IsOrderConnected α r] [Std.Trichotomous r] (x x_1 x_2 : List α),
  List.Lex r x x_2 → List.Lex r x x_1 ∨ List.Lex r x_1 x_2
-- Mathlib.Algebra.Ring.Ext
NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing_injective : ∀ {R : Type u}, Function.Injective (@NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing R)
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.Simp.dsimpMainCore : Lean.Expr →
  Lean.Meta.Simp.Context →
    optParam Lean.Meta.Simp.State { } →
      optParam Lean.Meta.Simp.Methods { } → Lean.MetaM (Lean.Expr × Lean.Meta.Simp.State)
-- Lean.Parser.Types
/-- Run `p` and record result in parser cache for any further invocation with this `parserName`, parser context, and parser state.
`p` cannot access syntax stack elements pushed before the invocation in order to make caching independent of parser history.
As this excludes trailing parsers from being cached, we also reset `lhsPrec`, which is not read but set by leading parsers, to 0
in order to increase cache hits. Finally, `errorMsg` is also reset to `none` as a leading parser should not be called in the first
place if there was an error.
 -/
Lean.Parser.withCache : Lean.Name → Lean.Parser.Parser → Lean.Parser.Parser
-- Init.Data.Range.Polymorphic.Map
/-- Compatibility class for `Map` and `Rxo.HasSize`.  -/
Std.PRange.UpwardEnumerable.Map.PreservesRxoSize : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Std.PRange.UpwardEnumerable α] →
      [inst_1 : Std.PRange.UpwardEnumerable β] →
        [Std.Rxo.HasSize α] → [Std.Rxo.HasSize β] → Std.PRange.UpwardEnumerable.Map α β → Prop
-- Mathlib.Order.GameAdd
Sym2.GameAdd.fst : ∀ {α : Type u_1} {rα : α → α → Prop} {a₁ a₂ b : α}, rα a₁ a₂ → Sym2.GameAdd rα s(a₁, b) s(a₂, b)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.restrict_spanning_iff : ∀ {α : Type u_2} {M : Matroid α} {R S : Set α},
  S ⊆ R → autoParam (R ⊆ M.E) Matroid.restrict_spanning_iff._auto_1 → ((M.restrict R).Spanning S ↔ R ⊆ M.closure S)
-- Lean.DocString.Parser
Lean.Doc.Parser.instBEqUnorderedListType : BEq Lean.Doc.Parser.UnorderedListType
-- Init.Data.Array.Lemmas
Array.mem_ite_empty_right : ∀ {α : Type u_1} {p : Prop} {x : α} [inst : Decidable p] {xs : Array α}, (x ∈ if p then xs else #[]) ↔ p ∧ x ∈ xs
-- Mathlib.Tactic.Translate.TagUnfoldBoundary
_private.Mathlib.Tactic.Translate.TagUnfoldBoundary.0.Mathlib.Tactic.Translate.CastKind.noConfusionType : Sort v✝ → Mathlib.Tactic.Translate.CastKind✝ → Mathlib.Tactic.Translate.CastKind✝ → Sort v✝
-- Mathlib.Algebra.Group.Units.Opposite
Units.opEquiv.eq_1 : ∀ {M : Type u_2} [inst : Monoid M],
  Units.opEquiv =
    {
      toFun := fun u =>
        MulOpposite.op { val := MulOpposite.unop ↑u, inv := MulOpposite.unop ↑u⁻¹, val_inv := ⋯, inv_val := ⋯ },
      invFun := fun X =>
        MulOpposite.rec' (fun u => { val := MulOpposite.op ↑u, inv := MulOpposite.op ↑u⁻¹, val_inv := ⋯, inv_val := ⋯ })
          X,
      left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthInf_exp : ∀ {a : EReal}, (ExpGrowth.expGrowthInf fun n => (a * ↑n).exp) = a
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.noZeroDivisors : NoZeroDivisors Cardinal.{u}
-- Lean.Compiler.ExternAttr
Lean.instBEqExternEntry.beq : Lean.ExternEntry → Lean.ExternEntry → Bool
-- Mathlib.Order.Filter.Ker
Filter.ker_pi : ∀ {ι : Type u_4} {α : ι → Type u_5} (f : (i : ι) → Filter (α i)), (Filter.pi f).ker = Set.univ.pi fun i => (f i).ker
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.balanceL!.match_5.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) →
      (l : Std.DTreeMap.Internal.Impl α β) →
        (Unit → motive Std.DTreeMap.Internal.Impl.leaf) →
          ((ls : ℕ) →
              (lk : α) →
                (lv : β lk) →
                  (ll lr : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr)) →
            motive l
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.hom_ext : ∀ {X Y : FinBddDistLat} {f g : X ⟶ Y}, FinBddDistLat.Hom.hom f = FinBddDistLat.Hom.hom g → f = g
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- The family of 2-morphisms out of a left Kan lift.  -/
CategoryTheory.Bicategory.LeftLift.IsKan.desc : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} →
        {g : c ⟶ a} →
          {t : CategoryTheory.Bicategory.LeftLift f g} →
            t.IsKan → (s : CategoryTheory.Bicategory.LeftLift f g) → t.lift ⟶ s.lift
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.getEntryD_eq_getEntryD : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [PartialEquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {fallback : (a : α) × β a},
      m.getEntryD a fallback = Std.Internal.List.getEntryD a fallback (Std.DHashMap.Internal.toListModel (↑m).buckets)
-- Mathlib.Combinatorics.Enumerative.Composition
_private.Mathlib.Combinatorics.Enumerative.Composition.0.Composition.recOnSingleAppend.match_1.eq_2 : ∀ (motive : (blocks : List ℕ) → (∀ {i : ℕ}, i ∈ blocks → 0 < i) → Sort u_1) (tail : List ℕ)
  (blocks_pos : ∀ {i : ℕ}, i ∈ 0 :: tail → 0 < i)
  (h_1 : (blocks_pos : ∀ {i : ℕ}, i ∈ [] → 0 < i) → motive [] blocks_pos)
  (h_2 : (tail : List ℕ) → (blocks_pos : ∀ {i : ℕ}, i ∈ 0 :: tail → 0 < i) → motive (0 :: tail) blocks_pos)
  (h_3 : (k : ℕ) → (l : List ℕ) → (blocks_pos : ∀ {i : ℕ}, i ∈ (k + 1) :: l → 0 < i) → motive (k.succ :: l) blocks_pos),
  (match 0 :: tail, blocks_pos with
    | [], blocks_pos => h_1 blocks_pos
    | 0 :: tail, blocks_pos => h_2 tail blocks_pos
    | k.succ :: l, blocks_pos => h_3 k l blocks_pos) =
    h_2 tail blocks_pos
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_filter_containsKey_of_containsKey_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₂ = true →
      Std.Internal.List.getEntry? k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) =
        Std.Internal.List.getEntry? k l₁
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.instFromJsonModuleHierarchy.fromJson : Lean.Json → Except String Lean.Lsp.Ipc.ModuleHierarchy
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.withConstants.eq_1 : ∀ (L : FirstOrder.Language) (α : Type w'), L.withConstants α = L.sum (FirstOrder.Language.constantsOn α)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rco_eq_nil : ∀ {m n : ℕ}, n ≤ m → (m...n).toList = []
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- **Alias** of the reverse direction of `SimpleGraph.cliqueFinset_eq_empty_iff`. -/
SimpleGraph.CliqueFree.cliqueFinset : ∀ {α : Type u_1} {G : SimpleGraph α} [inst : Fintype α] [inst_1 : DecidableEq α] [inst_2 : DecidableRel G.Adj] {n : ℕ},
  G.CliqueFree n → G.cliqueFinset n = ∅
-- Mathlib.Algebra.Category.Ring.FilteredColimits
/-- The colimit of `F ⋙ forget₂ RingCat SemiRingCat` in the category `SemiRingCat`.
In the following, we will show that this has the structure of a ring.
 -/
RingCat.FilteredColimits.R : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.IsFiltered J] → CategoryTheory.Functor J RingCat → SemiRingCat
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instBEqCode : {pu : Lean.Compiler.LCNF.Purity} → BEq (Lean.Compiler.LCNF.Code pu)
-- Mathlib.Analysis.Analytic.Order
/-- Simplifier lemma for the order of a centered monomial  -/
analyticOrderAt_centeredMonomial : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {z₀ : 𝕜} {n : ℕ}, analyticOrderAt ((fun x => x - z₀) ^ n) z₀ = ↑n
-- Init.Data.Slice.Lemmas
Std.Slice.size_toArray_eq_size : ∀ {γ : Type u} {α β : Type v} [inst : Std.ToIterator (Std.Slice γ) Id α β] [inst_1 : Std.Iterator α Id β]
  [inst_2 : Std.Slice.SliceSize γ] [Std.Slice.LawfulSliceSize γ] [Std.Iterators.Finite α Id] {s : Std.Slice γ},
  s.toArray.size = s.size
-- Mathlib.Order.Filter.IsBounded
Filter.isBounded_ge_atTop : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α], Filter.IsBounded (fun x1 x2 => x2 ≤ x1) Filter.atTop
-- Mathlib.Order.Filter.Cocardinal
Filter.compl_mem_cocardinal_of_card_lt : ∀ {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} {s : Set α}, Cardinal.mk ↑s < c → sᶜ ∈ Filter.cocardinal α hreg
-- Mathlib.Logic.Equiv.Bool
/-- The boolean negation function `not : Bool → Bool` is an involution and thus an equivalence.  -/
Equiv.boolNot : Equiv.Perm Bool
-- Mathlib.CategoryTheory.Galois.Action
CategoryTheory.PreGaloisCategory.functorToAction_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat) {X Y : C}
  (f : X ⟶ Y), ((CategoryTheory.PreGaloisCategory.functorToAction F).map f).hom = F.map f
-- Mathlib.Algebra.Homology.Embedding.TruncLE
/-- The canonical isomorphism `K.truncLE e ≅ (K.truncLE' e).extend e`.  -/
HomologicalComplex.truncLEIso : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              (K : HomologicalComplex C c') →
                (e : c.Embedding c') →
                  [inst_2 : e.IsTruncLE] →
                    [inst_3 : ∀ (i' : ι'), K.HasHomology i'] →
                      [inst_4 : CategoryTheory.Limits.HasZeroObject C] → K.truncLE e ≅ (K.truncLE' e).extend e
-- Init.Data.Range.Polymorphic.UInt
USize.instLawfulHasSize : Std.Rxc.LawfulHasSize USize
-- Mathlib.RepresentationTheory.Coinduced
Representation.coe_coindV : ∀ {k : Type u_1} {G : Type u_2} {H : Type u_3} [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : Monoid H] (φ : G →* H)
  {A : Type u_4} [inst_3 : AddCommMonoid A] [inst_4 : Module k A] (σ : Representation k G A),
  ↑(Representation.coindV φ σ) = {f | ∀ (g : G) (h : H), f (φ g * h) = (σ g) (f h)}
-- Batteries.Data.Fin.Basic
/-- Heterogeneous monadic fold over `Fin n` from right to left:
```
Fin.foldrM n f xₙ = do
  let xₙ₋₁ : α (n-1) ← f (n-1) xₙ
  let xₙ₋₂ : α (n-2) ← f (n-2) xₙ₋₁
  ...
  let x₀ : α 0 ← f 0 x₁
  pure x₀
```
This is the dependent version of `Fin.foldrM`.  -/
Fin.dfoldrM : {m : Type u_1 → Type u_2} →
  [Monad m] →
    (n : ℕ) → (α : Fin (n + 1) → Type u_1) → ((i : Fin n) → α i.succ → m (α i.castSucc)) → α (Fin.last n) → m (α 0)
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the largest key in the tree map, panicking if the map is
empty.
 -/
Std.DTreeMap.Raw.maxEntry! : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → [Inhabited ((a : α) × β a)] → Std.DTreeMap.Raw α β cmp → (a : α) × β a
-- Mathlib.Analysis.Analytic.Constructions
/-- Analytic functions on products are analytic in the first coordinate  -/
AnalyticOnNhd.curry_left : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E × F → G} {s : Set (E × F)} {y : F},
  AnalyticOnNhd 𝕜 f s → AnalyticOnNhd 𝕜 (fun x => f (x, y)) {x | (x, y) ∈ s}
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.sub_nat_mul_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [inst : NonAssocRing α],
  Function.Periodic f c → ∀ (n : ℕ), f (x - ↑n * c) = f x
-- Mathlib.Data.Finset.Slice
Finset.pairwiseDisjoint_slice : ∀ {α : Type u_1} {𝒜 : Finset (Finset α)}, Set.univ.PairwiseDisjoint 𝒜.slice
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
LinearIndependent.units_smul : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v : ι → M}, LinearIndependent R v → ∀ (w : ι → Rˣ), LinearIndependent R (w • v)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey!.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  (t t_1 : Std.ExtTreeMap α β cmp), t = t_1 → t.minKey! = t_1.minKey!
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionEqualizerProducts.piInters.hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  {F : TopCat.Presheaf C X} {ι : Type v'} {U : ι → TopologicalSpace.Opens ↑X} {X_1 : C}
  {f f' : X_1 ⟶ TopCat.Presheaf.SheafConditionEqualizerProducts.piInters F U},
  f = f' ↔
    ∀ (j : CategoryTheory.Discrete (ι × ι)),
      CategoryTheory.CategoryStruct.comp f
          (CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor fun p => F.obj (Opposite.op (U p.1 ⊓ U p.2)))
            j) =
        CategoryTheory.CategoryStruct.comp f'
          (CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor fun p => F.obj (Opposite.op (U p.1 ⊓ U p.2)))
            j)
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.norm_eq_zero_of_empty : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
  (f : BoundedContinuousFunction α β) [IsEmpty α], ‖f‖ = 0
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.L1.ofReal_norm_eq_lintegral : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  (f : ↥(MeasureTheory.Lp β 1 μ)), ENNReal.ofReal ‖f‖ = ∫⁻ (x : α), ‖↑↑f x‖ₑ ∂μ
-- Init.Tactics
/-- Syntax for excluding some names, e.g. `[-my_lemma, -my_theorem]`.
 -/
Lean.Parser.Tactic.rewrites_forbidden : Lean.ParserDescr
-- Mathlib.Order.CompleteBooleanAlgebra
disjoint_iSup_iff : ∀ {α : Type u} {ι : Sort w} [inst : Order.Frame α] {a : α} {f : ι → α},
  Disjoint a (⨆ i, f i) ↔ ∀ (i : ι), Disjoint a (f i)
-- Mathlib.Data.Set.Basic
/-- See also `Set.nonempty_iff_ne_empty`.  -/
Set.not_nonempty_iff_eq_empty : ∀ {α : Type u} {s : Set α}, ¬s.Nonempty ↔ s = ∅
-- Mathlib.Data.Complex.Basic
/-- The imaginary part of a complex number.  -/
Complex.im : ℂ → ℝ
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
contravariant_lt_of_covariant_le : ∀ (N : Type u_2) (mu : N → N → N) [inst : LinearOrder N] [CovariantClass N N mu fun x1 x2 => x1 ≤ x2],
  ContravariantClass N N mu fun x1 x2 => x1 < x2
-- Mathlib.Algebra.Algebra.Opposite
RingHom.toOpposite.congr_simp : ∀ {R : Type u_2} {S : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] (f f_1 : R →+* S) (e_f : f = f_1)
  (hf : ∀ (x y : R), Commute (f x) (f y)), f.toOpposite hf = f_1.toOpposite ⋯
-- Mathlib.Algebra.Group.Hom.Defs
AddHom.comp_apply : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (g : N →ₙ+ P)
  (f : M →ₙ+ N) (x : M), (g.comp f) x = g (f x)
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.eq_top_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C),
  J = ⊤ ↔ ∀ (X : C), ⊥ ∈ J X
-- Init.Data.Int.Order
Int.add_neg_of_nonpos_of_neg : ∀ {a b : ℤ}, a ≤ 0 → b < 0 → a + b < 0
-- Mathlib.Tactic.ApplyCongr
/-- Apply a congruence lemma inside `conv` mode.

When called without an argument `apply_congr` will try applying all lemmas marked with `@[congr]`.
Otherwise `apply_congr e` will apply the lemma `e`.

Recall that a goal that appears as `∣ X` in `conv` mode
represents a goal of `⊢ X = ?m`,
i.e. an equation with a metavariable for the right-hand side.

To successfully use `apply_congr e`, `e` will need to be an equation
(possibly after function arguments),
which can be unified with a goal of the form `X = ?m`.
The right-hand side of `e` will then determine the metavariable,
and `conv` will subsequently replace `X` with that right-hand side.

As usual, `apply_congr` can create new goals;
any of these which are _not_ equations with a metavariable on the right-hand side
will be hard to deal with in `conv` mode.
Thus `apply_congr` automatically calls `intros` on any new goals,
and fails if they are not then equations.

In particular it is useful for rewriting inside the operand of a `Finset.sum`,
as it provides an extra hypothesis asserting we are inside the domain.

For example:

```lean
example (f g : ℤ → ℤ) (S : Finset ℤ) (h : ∀ m ∈ S, f m = g m) :
    Finset.sum S f = Finset.sum S g := by
  conv_lhs =>
    -- If we just call `congr` here, in the second goal we're helpless,
    -- because we are only given the opportunity to rewrite `f`.
    -- However `apply_congr` uses the appropriate `@[congr]` lemma,
    -- so we get to rewrite `f x`, in the presence of the crucial `H : x ∈ S` hypothesis.
    apply_congr
    · skip
    · simp [*]
```

In the above example, when the `apply_congr` tactic is called it gives the hypothesis `H : x ∈ S`
which is then used to rewrite the `f x` to `g x`.
 -/
Lean.Elab.Tactic.applyCongr : Option Lean.Expr → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
SSet.finite_of_isColimit : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} J] [CategoryTheory.Limits.HasColimitsOfShape J (Type u)]
  {F : CategoryTheory.Functor J SSet} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c)
  [Finite J], (∀ (j : J), (F.obj j).Finite) → c.pt.Finite
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
/-- Further truncating `X` above `m` does not change the `m`-spine.  -/
SSet.Truncated.trunc_spine : ∀ {n : ℕ} (X : SSet.Truncated (n + 1)) (k m : ℕ) (h : m ≤ k + 1) (hₙ : k ≤ n),
  ((SSet.Truncated.trunc (n + 1) (k + 1) ⋯).obj X).spine m h = X.spine m ⋯
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.constGetD_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α} {fallback : β},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → Std.DTreeMap.Raw.Const.getD t₁ k fallback = Std.DTreeMap.Raw.Const.getD t₂ k fallback
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.coe_derivedSeries_one_eq : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  (LieIdeal.toLieSubalgebra R L (LieAlgebra.derivedSeries R L 1)).toSubmodule =
    Submodule.span R {x | ∃ x_1 y, ⁅x_1, y⁆ = x}
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.instCoeAlgHom : {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] → Coe (A →A[R] B) (A →ₐ[R] B)
-- Std.Time.Format.Modifier
/-- Full form of the localized offset (e.g., "GMT+08:00")
 -/
Std.Time.OffsetO.full : Std.Time.OffsetO
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.Hom.mk.inj : ∀ {X Y : SFinKer} {hom : ProbabilityTheory.Kernel X.carrier Y.carrier}
  {property : ProbabilityTheory.IsSFiniteKernel hom} {hom_1 : ProbabilityTheory.Kernel X.carrier Y.carrier}
  {property_1 : ProbabilityTheory.IsSFiniteKernel hom_1},
  { hom := hom, property := property } = { hom := hom_1, property := property_1 } → hom = hom_1
-- Mathlib.RingTheory.Valuation.Discrete.Basic
/-- Given a discrete valuation `v`, `Valuation.IsRankOneDiscrete.generator` is a generator of
the value group that is `< 1`, as an element of `valueGroup v`.  -/
Valuation.IsRankOneDiscrete.generator' : {Γ : Type u_1} →
  [inst : LinearOrderedCommGroupWithZero Γ] →
    {A : Type u_2} →
      [inst_1 : Ring A] → (v : Valuation A Γ) → [v.IsRankOneDiscrete] → ↥(MonoidWithZeroHom.ofClass v).valueGroup