mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.ENNReal.Inv
/-- See `ENNReal.inv_mul_cancel_right` for a simpler version assuming `b ≠ 0`, `b ≠ ∞`.  -/
ENNReal.inv_mul_cancel_right' : ∀ {a b : ENNReal}, (b = 0 → a = 0) → (b = ⊤ → a = 0) → a * b⁻¹ * b = a
-- Init.Data.UInt.Bitwise
UInt64.ofNat_shiftLeft : ∀ (a b : ℕ), b < 64 → UInt64.ofNat (a <<< b) = UInt64.ofNat a <<< UInt64.ofNat b
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.le_max!_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {k : α}, k ∈ t → (cmp k t.max!).isLE = true
-- Mathlib.Dynamics.Minimal
AddAction.isMinimal_of_pretransitive : ∀ (M : Type u_1) {α : Type u_3} [inst : AddMonoid M] [inst_1 : TopologicalSpace α] [inst_2 : AddAction M α]
  [AddAction.IsPretransitive M α], AddAction.IsMinimal M α
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
measurable_of_isClosed' : ∀ {γ : Type u_3} {δ : Type u_5} [inst : TopologicalSpace γ] [inst_1 : MeasurableSpace γ] [BorelSpace γ]
  [inst_3 : MeasurableSpace δ] {f : δ → γ},
  (∀ (s : Set γ), IsClosed s → s.Nonempty → s ≠ Set.univ → MeasurableSet (f ⁻¹' s)) → Measurable f
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.map_comp_eq : ∀ {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z),
  TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp f g) =
    (TopologicalSpace.Opens.map g).comp (TopologicalSpace.Opens.map f)
-- Mathlib.Computability.StateTransition
/-- Given a relation `tr : σ₁ → σ₂ → Prop` between state spaces, and state transition functions
`f₁ : σ₁ → Option σ₁` and `f₂ : σ₂ → Option σ₂`, `Respects f₁ f₂ tr` means that if `tr a₁ a₂` holds
initially and `f₁` takes a step to `a₂` then `f₂` will take one or more steps before reaching a
state `b₂` satisfying `tr a₂ b₂`, and if `f₁ a₁` terminates then `f₂ a₂` also terminates.
Such a relation `tr` is also known as a refinement.  -/
StateTransition.Respects : {σ₁ : Type u_1} → {σ₂ : Type u_2} → (σ₁ → Option σ₁) → (σ₂ → Option σ₂) → (σ₁ → σ₂ → Prop) → Prop
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.op : Cᵒᵖ ⥤ Dᵒᵖ` reflects limits, then `F : C ⥤ D` reflects colimits.  -/
CategoryTheory.Limits.reflectsColimits_of_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsLimits F.op], CategoryTheory.Limits.ReflectsColimits F
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Iso.mapEdgeSet_symm_apply : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') (e : ↑G'.edgeSet),
  f.mapEdgeSet.symm e = SimpleGraph.Hom.mapEdgeSet (RelIso.toRelEmbedding f.symm).toRelHom e
-- Mathlib.Data.Finsupp.Defs
Finsupp.mapRange_bijective : ∀ {α : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] (e : M → N) (he₀ : e 0 = 0),
  Function.Bijective e → Function.Bijective (Finsupp.mapRange e he₀)
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
/-- The Galois connection between fixing subgroups and fixed points of a group action  -/
fixingSubgroup_fixedPoints_gc : ∀ (M : Type u_1) (α : Type u_2) [inst : Group M] [inst_1 : MulAction M α],
  GaloisConnection (⇑OrderDual.toDual ∘ fixingSubgroup M) ((fun P => MulAction.fixedPoints (↥P) α) ∘ ⇑OrderDual.ofDual)
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_right : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ : Int.Internal.Linear.Poly) (n : ℕ),
  Int.Internal.Linear.cooper_right_cert p₁ p₂ n = true →
    Int.Internal.Linear.Poly.denote' ctx p₁ ≤ 0 →
      Int.Internal.Linear.Poly.denote' ctx p₂ ≤ 0 →
        Int.Internal.Linear.OrOver n (Int.Internal.Linear.cooper_right_split ctx p₁ p₂)
-- Mathlib.Tactic.Variable
/-- Hint for the unused variables linter. Copies the one for `variable`.  -/
Mathlib.Command.Variable.ignorevariable? : Lean.Linter.IgnoreFunction
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.eq_of_lt : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) [Ring.KrullDimLE 1 ↥A] {B : ValuationSubring K}, A < B → B = ⊤
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.instIsAffineXSchemeFiniteSubcover : ∀ (X : AlgebraicGeometry.Scheme) [inst : CompactSpace ↥X] (𝒰 : X.OpenCover)
  [∀ (i : 𝒰.I₀), AlgebraicGeometry.IsAffine (𝒰.X i)] (i : 𝒰.finiteSubcover.I₀),
  AlgebraicGeometry.IsAffine (𝒰.finiteSubcover.X i)
-- Mathlib.Tactic.CrossRefAttribute
/-- The display label used in docstring links and trace output.  -/
Mathlib.CrossRef.Database.label : Mathlib.CrossRef.Database → String
-- Mathlib.Order.BoundedOrder.Lattice
WellFoundedGT.induction_top : ∀ {α : Type u_1} [inst : Preorder α] [WellFoundedGT α] [inst_2 : OrderTop α] {P : α → Prop},
  (∃ M, P M) → (∀ (N : α), N ≠ ⊤ → P N → ∃ M > N, P M) → P ⊤
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
orthogonalBilin_innerₗ : ∀ {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] (K : Submodule ℝ E),
  Submodule.orthogonalBilin (innerₗ E) K = Kᗮ
-- Init.Data.UInt.Lemmas
UInt64.ofNat_uInt32ToNat : ∀ (n : UInt32), UInt64.ofNat n.toNat = n.toUInt64
-- Mathlib.NumberTheory.ModularForms.Basic
/-- The constant function with value `x : ℂ` as a modular form of weight 0 and any level.  -/
ModularForm.const : {Γ : Subgroup (GL (Fin 2) ℝ)} → ℂ → [Γ.HasDetOne] → ModularForm Γ 0
-- Mathlib.Combinatorics.SimpleGraph.LapMatrix
/-- The diagonal matrix consisting of the degrees of the vertices in the graph.  -/
SimpleGraph.degMatrix : {V : Type u_1} →
  (R : Type u_2) →
    [Fintype V] → (G : SimpleGraph V) → [DecidableRel G.Adj] → [DecidableEq V] → [AddMonoidWithOne R] → Matrix V V R
-- Lean.EnvExtension
Lean.MapDeclarationExtension.mk.injEq : ∀ {α : Type}
  (toPersistentEnvExtension toPersistentEnvExtension_1 :
    Lean.PersistentEnvExtension (Lean.Name × α) (Lean.Name × α) (Lean.NameMap α)),
  ({ toPersistentEnvExtension := toPersistentEnvExtension } =
      { toPersistentEnvExtension := toPersistentEnvExtension_1 }) =
    (toPersistentEnvExtension = toPersistentEnvExtension_1)
-- Batteries.Data.List.Lemmas
List.max!_eq_max?_getD : ∀ {α : Type u_1} [inst : Inhabited α] {l : List α} [inst_1 : Max α], l.max! = l.max?.getD default
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.State.f : Lean.Elab.Tactic.ElimApp.State✝ → Lean.Expr
-- Mathlib.Algebra.Order.GroupWithZero.Defs
/-- Pullback `MulPosMono`.  -/
Function.Injective.mulPosMono : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [MulPosMono α] {β : Type u_2} [inst_4 : Zero β]
  [inst_5 : Mul β] [inst_6 : Preorder β] (f : β → α),
  f 0 = 0 → (∀ (x y : β), f (x * y) = f x * f y) → (∀ {x y : β}, f x ≤ f y ↔ x ≤ y) → MulPosMono β
-- Mathlib.CategoryTheory.Galois.Decomposition
/-- For each `x : F.obj X`, this is the composition of `u` with the projection at `x`.  -/
_private.Mathlib.CategoryTheory.Galois.Decomposition.0.CategoryTheory.PreGaloisCategory.selfProdProj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      {F : CategoryTheory.Functor C FintypeCat} →
        {X A : C} → (A ⟶ CategoryTheory.PreGaloisCategory.selfProd✝ F X) → (F.obj X).obj → (A ⟶ X)
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
CategoryTheory.PreOneHypercover.cylinderHom_h₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} [inst_1 : CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F)
  {p q : (CategoryTheory.PreOneHypercover.cylinder f g).I₀} (k : (CategoryTheory.PreOneHypercover.cylinder f g).I₁ p q),
  (CategoryTheory.PreOneHypercover.cylinderHom f g).h₁ k =
    CategoryTheory.Limits.pullback.snd
      (CategoryTheory.Limits.pullback.map (CategoryTheory.PreOneHypercover.cylinderf f g p.snd)
        (CategoryTheory.PreOneHypercover.cylinderf f g q.snd) (E.f p.fst) (E.f q.fst)
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯)
          (F.toPullback p.snd))
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯)
          (F.toPullback q.snd))
        (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
      (CategoryTheory.Limits.pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯)
-- Mathlib.Topology.Algebra.Group.GroupTopology
/-- Infimum of a collection of group topologies.  -/
GroupTopology.instInfSet : {α : Type u} → [inst : Group α] → InfSet (GroupTopology α)
-- Lean.Data.Lsp.TextSync
Lean.Lsp.DidCloseTextDocumentParams.mk : Lean.Lsp.TextDocumentIdentifier → Lean.Lsp.DidCloseTextDocumentParams
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.shiftIso_zero : ∀ {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] (a : M),
  F.shiftIso 0 a a ⋯ =
    CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.shiftFunctorZero C M) (F.shift a) ≪≫ (F.shift a).leftUnitor
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.FinitenessRelation : {α : Type u} → {β : α → Type v} → Std.Iterators.FinitenessRelation (Std.DTreeMap.Internal.Zipper α β) Id
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Module.instFintypeElemExtendOfFiniteSubtypeMemSubmoduleSpan : {R : Type u_2} →
  {M : Type u_3} →
    [inst : DivisionRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {s t : Set M} →
            [Module.Finite R ↥(Submodule.span R t)] →
              (hs : LinearIndepOn R id s) → (hst : s ⊆ t) → Fintype ↑(hs.extend hst)
-- Mathlib.Topology.LocallyFinsupp
/-- A function `f : X → Y` has locally finite support if for every `z : X`, there is a
neighbourhood `t` around `z` such that `t ∩ f.support` is finite.
 -/
LocallyFiniteSupport : {X : Type u_1} → [TopologicalSpace X] → {Y : Type u_2} → [Zero Y] → (X → Y) → Prop
-- Mathlib.CategoryTheory.Shift.Pullback
/-- The category `PullbackShift C φ` is equipped with a shift such that for all `a`,
the shift functor by `a` is `shiftFunctor C (φ a)`.  -/
CategoryTheory.PullbackShift : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {A : Type u_2} →
      {B : Type u_3} →
        [inst_1 : AddMonoid A] → [inst_2 : AddMonoid B] → [CategoryTheory.HasShift C B] → (A →+ B) → Type u_1
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
/-- Scalar multiplication by `ℂ`, assuming that `Γ ⊆ SL(2, ℝ)`.  -/
SlashInvariantForm.instSMul : {Γ : Subgroup (GL (Fin 2) ℝ)} →
  {k : ℤ} → [Γ.HasDetOne] → {α : Type u_2} → [inst : SMul α ℂ] → [IsScalarTower α ℂ ℂ] → SMul α (SlashInvariantForm Γ k)
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.instGroup : {G : Type u_1} → [inst : Add G] → {a : G} → Group (AddConstEquiv G G a a)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- The `enorm` of a strongly a.e. measurable function is a.e. measurable.

Note that unlike `AEStronglyMeasurable.norm` and `AEStronglyMeasurable.nnnorm`, this lemma proves
a.e. measurability, **not** a.e. strong measurability. This is an intentional decision:
for functions taking values in `ℝ≥0∞`, a.e. measurability is much more useful than
a.e. strong measurability.  -/
MeasureTheory.AEStronglyMeasurable.enorm : ∀ {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [inst : TopologicalSpace β]
  [inst_1 : ContinuousENorm β] {f : α → β}, MeasureTheory.AEStronglyMeasurable f μ → AEMeasurable (fun x => ‖f x‖ₑ) μ
-- Mathlib.Topology.UniformSpace.Separation
inseparable_iff_clusterPt_uniformity : ∀ {α : Type u} [inst : UniformSpace α] {x y : α}, Inseparable x y ↔ ClusterPt (x, y) (uniformity α)
-- Mathlib.Algebra.Notation.Indicator
/-- If a multiplicative indicator function is not equal to `1` at a point, then that point is in the
set.  -/
Set.mem_of_mulIndicator_ne_one : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] {s : Set α} {f : α → M} {a : α}, s.mulIndicator f a ≠ 1 → a ∈ s
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.mem_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool} {k : α},
  k ∈ Std.ExtDHashMap.filter f m ↔ ∃ (h' : k ∈ m), f (m.getKey k h') (Std.ExtDHashMap.Const.get m k h') = true
-- Mathlib.Order.MinMax
max_le_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, max a b ≤ c ↔ a ≤ c ∧ b ≤ c
-- Mathlib.NumberTheory.ZetaValues
bernoulliFun_two : ∀ (x : ℝ), bernoulliFun 2 x = x ^ 2 - x + 6⁻¹
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.map_add_toArray_roc' : ∀ {m n k : ℕ}, Array.map (fun x => k + x) (m<...=n).toArray = ((k + m)<...=k + n).toArray
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.S.eq_iff_ofSimplex_eq : ∀ {X : SSet} {n m : ℕ} (x : X.obj (Opposite.op { len := n })) (y : X.obj (Opposite.op { len := m })),
  x ∈ X.nonDegenerate n →
    y ∈ X.nonDegenerate m →
      ({ dim := n, simplex := x } = { dim := m, simplex := y } ↔
        SSet.Subcomplex.ofSimplex x = SSet.Subcomplex.ofSimplex y)
-- Mathlib.Data.List.Perm.Basic
List.Perm.product_left : ∀ {α : Type u_1} {β : Type u_2} (l : List α) {t₁ t₂ : List β}, t₁.Perm t₂ → (l.product t₁).Perm (l.product t₂)
-- Mathlib.Geometry.Convex.Cone.Face.Basic
PointedCone.IsFaceOf.of_comap_surjective : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {C F : PointedCone R M} [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] {f : N →ₗ[R] M},
  Function.Surjective ⇑f → (PointedCone.comap f F).IsFaceOf (PointedCone.comap f C) → F.IsFaceOf C
-- Mathlib.CategoryTheory.Category.Preorder
OrderIso.equivalence_inverse : ∀ {X : Type u} {Y : Type v} [inst : Preorder X] [inst_1 : Preorder Y] (e : X ≃o Y), e.equivalence.inverse = ⋯.functor
-- Mathlib.Order.WithBot
WithTop.le_untop_iff : ∀ {α : Type u_1} {a : α} [inst : LE α] {x : WithTop α} (hx : x ≠ ⊤), a ≤ x.untop hx ↔ ↑a ≤ x
-- Lean.Elab.DocString
/-- Built-in code suggestions, for bootstrapping
 -/
Lean.Doc.builtinCodeSuggestions : IO.Ref (Array (Lean.Name × Lean.Doc.CodeSuggester))
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instHashableCompletionIdentifier.hash : Lean.Lsp.CompletionIdentifier → UInt64
-- Mathlib.Data.Nat.Init
Nat.succ_pos' : ∀ {n : ℕ}, 0 < n.succ
-- Mathlib.Data.Set.Finite.Basic
/-- Embedding of `ℕ` into an infinite set.  -/
Set.Infinite.natEmbedding : {α : Type u} → (s : Set α) → s.Infinite → ℕ ↪ ↑s
-- Batteries.Lean.Meta.Inaccessible
/-- Obtain the inaccessible fvars from the current local context. An fvar is
inaccessible if (a) its user name is inaccessible or (b) it is shadowed by a
later fvar with the same user name.
 -/
Lean.Meta.getInaccessibleFVars : {m : Type → Type} → [Monad m] → [Lean.MonadLCtx m] → m (Array Lean.LocalDecl)
-- Mathlib.CategoryTheory.ConcreteCategory.Forget
/-- **Alias** of `CategoryTheory.ObjectProperty.FullSubcategory.hasForget₂`. -/
CategoryTheory.FullSubcategory.hasForget₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {FC : outParam (C → C → Type u_2)} →
      {CC : outParam (C → Type w)} →
        [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] →
          [inst_2 : CategoryTheory.ConcreteCategory C FC] →
            (P : CategoryTheory.ObjectProperty C) → CategoryTheory.HasForget₂ P.FullSubcategory C
-- Lean.Meta.Tactic.Grind.Types
/-- Returns node associated with `e`. It assumes `e` has already been internalized.  -/
Lean.Meta.Grind.getENode : Lean.Expr → Lean.Meta.Grind.GoalM Lean.Meta.Grind.ENode
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.instIsIntegral : ∀ {n : Type u} (S : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral S],
  AlgebraicGeometry.IsIntegral (AlgebraicGeometry.AffineSpace n S)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.conePointUniqueUpToIso_inv_comp_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F] {c : CategoryTheory.Limits.Cone F}
  (hc : CategoryTheory.Limits.IsLimit c) (j : J) {Z : C} (h : F.obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.limit.isLimit F).conePointUniqueUpToIso hc).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j) h) =
    CategoryTheory.CategoryStruct.comp (c.π.app j) h
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.go.match_13.eq_3 : ∀ (motive : Std.Sat.AIG.Decl ℕ → Sort u_1) (lhs rhs : Std.Sat.AIG.Fanin)
  (h_1 : Std.Sat.AIG.Decl.gate lhs rhs = Std.Sat.AIG.Decl.false → motive Std.Sat.AIG.Decl.false)
  (h_2 : (idx : ℕ) → Std.Sat.AIG.Decl.gate lhs rhs = Std.Sat.AIG.Decl.atom idx → motive (Std.Sat.AIG.Decl.atom idx))
  (h_3 :
    (lhs_1 rhs_1 : Std.Sat.AIG.Fanin) →
      Std.Sat.AIG.Decl.gate lhs rhs = Std.Sat.AIG.Decl.gate lhs_1 rhs_1 → motive (Std.Sat.AIG.Decl.gate lhs_1 rhs_1)),
  (match heq : Std.Sat.AIG.Decl.gate lhs rhs with
    | Std.Sat.AIG.Decl.false => h_1 heq
    | Std.Sat.AIG.Decl.atom idx => h_2 idx heq
    | Std.Sat.AIG.Decl.gate lhs_1 rhs_1 => h_3 lhs_1 rhs_1 heq) =
    h_3 lhs rhs ⋯
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.pow_const : ∀ {β : Type u_2} {γ : Type u_3} {α : Type u_4} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ]
  [inst_2 : Pow β γ] [MeasurablePow β γ] {m : MeasurableSpace α} {f : α → β},
  Measurable f → ∀ (c : γ), Measurable fun x => f x ^ c
-- Mathlib.Algebra.Order.CauSeq.Basic
rat_inv_continuous_lemma : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {β : Type u_3}
  [inst_3 : DivisionRing β] (abv : β → α) [IsAbsoluteValue abv] {ε K : α},
  0 < ε → 0 < K → ∃ δ > 0, ∀ {a b : β}, K ≤ abv a → K ≤ abv b → abv (a - b) < δ → abv (a⁻¹ - b⁻¹) < ε
-- Mathlib.GroupTheory.Exponent
/-- If `H` is a normal subgroup of `G`, then the exponent of `G ⧸ H` divides the exponent of `G`.
 -/
Group.exponent_quotient_dvd : ∀ {G : Type u} [inst : Group G] (H : Subgroup G) [inst_1 : H.Normal], Monoid.exponent (G ⧸ H) ∣ Monoid.exponent G
-- Mathlib.Tactic.Choose
/-- Optional expected type annotation  -/
Mathlib.Tactic.Choose.ChooseArg.expectedType? : Mathlib.Tactic.Choose.ChooseArg → Option Lean.Term
-- Mathlib.LinearAlgebra.Dimension.Finite
/-- A finite-dimensional space is nontrivial if it has `finrank` equal to the successor of a
natural number.  -/
Module.nontrivial_of_finrank_eq_succ : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial R] {n : ℕ},
  Module.finrank R M = n.succ → Nontrivial M
-- Mathlib.Order.KrullDimension
Order.coheight_le : ∀ {α : Type u_1} [inst : Preorder α] {a : α} {n : ℕ∞},
  (∀ (p : LTSeries α), RelSeries.head p = a → ↑p.length ≤ n) → Order.coheight a ≤ n
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.Full.id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C], (CategoryTheory.Functor.id C).Full
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
SummableLocallyUniformlyOn.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] (f : ι → β → α) (s : Set β)
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β],
  SummableLocallyUniformlyOn f s = ∃ g, HasSumLocallyUniformlyOn f g s
-- Mathlib.RingTheory.Finiteness.Prod
Submodule.FG.prod : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {P : Type u_3}
  [inst_3 : AddCommMonoid P] [inst_4 : Module R P] {sb : Submodule R M} {sc : Submodule R P},
  sb.FG → sc.FG → (sb.prod sc).FG
-- Mathlib.Data.Fin.Tuple.Take
Fin.take_repeat : ∀ {n : ℕ} {α : Type u_2} {n' : ℕ} (m : ℕ) (h : m ≤ n) (a : Fin n' → α),
  Fin.take (m * n') ⋯ (Fin.repeat n a) = Fin.repeat m a
-- Aesop.RuleTac.ElabRuleTerm
Aesop.elabRuleTermForApplyLikeMetaM : Lean.MVarId → Lean.Term → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroupClass.toAddGroup.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {S : Type u_4} (H : S) [inst_1 : SetLike S G] [inst_2 : AddSubgroupClass S G],
  AddSubgroupClass.toAddGroup H =
    { toAddMonoid := AddSubmonoidClass.toAddMonoid H, toNeg := NegMemClass.neg, toSub := AddSubgroupClass.sub,
      toZSMul := ZSMul.ofSMul, sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯,
      neg_add_cancel := ⋯ }
-- Mathlib.Topology.DenseEmbedding
Dense.isDenseInducing_val : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α}, Dense s → IsDenseInducing Subtype.val
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
Nat.Partition.ofSym_one : ∀ {σ : Type u_1} [inst : DecidableEq σ] (s : Sym σ 1), Nat.Partition.ofSym s = Nat.Partition.indiscrete 1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- If `f₁ = f₂` and `g₁ = g₂`, we may construct a canonical
isomorphism `pullback f₁ g₁ ≅ pullback f₂ g₂`  -/
CategoryTheory.Limits.pullback.congrHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f₁ f₂ : X ⟶ Z} →
        {g₁ g₂ : Y ⟶ Z} →
          f₁ = f₂ →
            g₁ = g₂ →
              [inst_1 : CategoryTheory.Limits.HasPullback f₁ g₁] →
                [inst_2 : CategoryTheory.Limits.HasPullback f₂ g₂] →
                  CategoryTheory.Limits.pullback f₁ g₁ ≅ CategoryTheory.Limits.pullback f₂ g₂
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.mul_card_le_expansion : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {K : ℝ} {A S : Finset G},
  S.Nonempty → (1 - K) * ↑A.card ≤ Finset.expansion✝ K S A
-- Mathlib.Data.Set.Image
Set.disjoint_image_inl_range_inr : ∀ {α : Type u_1} {β : Type u_2} {u : Set α}, Disjoint (Sum.inl '' u) (Set.range Sum.inr)
-- Mathlib.Combinatorics.Additive.Corner.Roth
/-- An explicit form for the constant in the corners theorem.

Note that this depends on `SzemerediRegularity.bound`, which is a tower-type exponential. This means
`cornersTheoremBound` is in practice absolutely tiny.  -/
cornersTheoremBound : ℝ → ℕ
-- Mathlib.Topology.Order.Hom.Basic
ContinuousOrderHom.mk.inj : ∀ {α : Type u_6} {β : Type u_7} {inst : Preorder α} {inst_1 : Preorder β} {inst_2 : TopologicalSpace α}
  {inst_3 : TopologicalSpace β} {toOrderHom : α →o β} {continuous_toFun : Continuous toOrderHom.toFun}
  {toOrderHom_1 : α →o β} {continuous_toFun_1 : Continuous toOrderHom_1.toFun},
  { toOrderHom := toOrderHom, continuous_toFun := continuous_toFun } =
      { toOrderHom := toOrderHom_1, continuous_toFun := continuous_toFun_1 } →
    toOrderHom = toOrderHom_1
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.singleton_injective : Function.Injective singleton
-- Mathlib.RingTheory.Smooth.Locus
Algebra.smoothLocus_comap_of_isLocalization : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {Af : Type u_3}
  [inst_3 : CommRing Af] [inst_4 : Algebra A Af] [inst_5 : Algebra R Af] [IsScalarTower R A Af] (f : A)
  [IsLocalization.Away f Af],
  PrimeSpectrum.comap (algebraMap A Af) ⁻¹' Algebra.smoothLocus R A = Algebra.smoothLocus R Af
-- Lean.Meta.LazyDiscrTree
/-- Discrimination tree key.
 -/
Lean.Meta.LazyDiscrTree.Key : Type
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.id_toLinearMap : ∀ {R : Type u_1} {E : Type u_5} [inst : Semiring R] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module R E],
  LinearIsometry.id.toLinearMap = LinearMap.id
-- Mathlib.Data.Seq.Computation
Computation.Bind.f.eq_1 : ∀ {α : Type u} {β : Type v} (f : α → Computation β) (ca : Computation α),
  Computation.Bind.f f (Sum.inl ca) =
    match ca.destruct with
    | Sum.inl a => Computation.Bind.g (f a).destruct
    | Sum.inr ca' => Sum.inr (Sum.inl ca')
-- Mathlib.Analysis.InnerProductSpace.Dual
/-- A nonzero rank-one operator has rank one.  -/
InnerProductSpace.rank_rankOne : ∀ {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] {x : E} {y : F},
  x ≠ 0 → y ≠ 0 → (↑(((InnerProductSpace.rankOne 𝕜) x) y)).rank = 1