mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
/-- If `f : R → ℝ` is a nonnegative, multiplicatively bounded function, then for every `x : R`,
`f x ≤ f 1 * seminormFromBounded' f x`.  -/
seminormFromBounded_ge : ∀ {R : Type u_1} [inst : CommRing R] {f : R → ℝ} {c : ℝ},
  0 ≤ f → (∀ (x y : R), f (x * y) ≤ c * f x * f y) → ∀ (x : R), f x ≤ f 1 * seminormFromBounded' f x
-- Mathlib.Data.Set.Monotone
MonotoneOn.congr : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β} [inst : Preorder α] [inst_1 : Preorder β],
  MonotoneOn f₁ s → Set.EqOn f₁ f₂ s → MonotoneOn f₂ s
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.size_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, (m.insert k).size = if k ∈ m then m.size else m.size + 1
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.map_apply : ∀ {m₁ m₂ : SimplexCategoryᵒᵖ} (f : m₁ ⟶ m₂) {n : SimplexCategory} (x : (SSet.stdSimplex.obj n).obj m₁),
  (CategoryTheory.ConcreteCategory.hom ((SSet.stdSimplex.obj n).map f)) x =
    SSet.stdSimplex.objEquiv.symm (CategoryTheory.CategoryStruct.comp f.unop (SSet.stdSimplex.objEquiv x))
-- Mathlib.Order.SetAccumulate
/-- For a directed set of sets `s : ℕ → Set α` and `n : ℕ`, there exists `m : ℕ` (maybe
larger than `n`) such that `accumulate s n ⊆ s m`.  -/
Set.exists_subset_accumulate_of_directed : ∀ {α : Type u_1} {s : ℕ → Set α}, Directed (fun x1 x2 => x1 ⊆ x2) s → ∀ (n : ℕ), ∃ m, Set.accumulate s n ⊆ s m
-- Mathlib.Tactic.NormNum.BigOperators
/-- If `s = t` and we can get the result for `t`, then we can get the result for `s`.
 -/
Mathlib.Meta.Finset.ProveEmptyOrConsResult.eq_trans : {u : Lean.Level} →
  {α : Q(Type u)} →
    {s t : Q(Finset «$α»)} →
      Q(«$s» = «$t») → Mathlib.Meta.Finset.ProveEmptyOrConsResult t → Mathlib.Meta.Finset.ProveEmptyOrConsResult s
-- Aesop.Tree.Data
Aesop.GoalData.children : {Rapp MVarCluster : Type} → Aesop.GoalData Rapp MVarCluster → Array (IO.Ref Rapp)
-- Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
GaussianFourier.integral_cexp_neg_mul_sq_norm_add : ∀ {b : ℂ} {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : FiniteDimensional ℝ V]
  [inst_3 : MeasurableSpace V] [inst_4 : BorelSpace V],
  0 < b.re →
    ∀ (c : ℂ) (w : V),
      ∫ (v : V), Complex.exp (-b * ↑‖v‖ ^ 2 + c * ↑(inner ℝ w v)) =
        (↑Real.pi / b) ^ (↑(Module.finrank ℝ V) / 2) * Complex.exp (c ^ 2 * ↑‖w‖ ^ 2 / (4 * b))
-- Mathlib.RingTheory.Perfection
Perfection.coeffMonoidHom_mk : ∀ {M : Type u_1} [inst : CommMonoid M] {p : ℕ} (f : ℕ → M) (hf : ∀ (n : ℕ), f (n + 1) ^ p = f n) (n : ℕ),
  (Perfection.coeffMonoidHom M p n) ⟨f, hf⟩ = f n
-- Mathlib.Combinatorics.Graph.Basic
Graph.ext_iff : ∀ {α : Type u_1} {β : Type u_2} {G₁ G₂ : Graph α β},
  G₁ = G₂ ↔ G₁.vertexSet = G₂.vertexSet ∧ ∀ (e : β) (x y : α), G₁.IsLink e x y ↔ G₂.IsLink e x y
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.coe_smul : ∀ {R : Type u_1} [inst : Ring R] (I : TwoSidedIdeal R) {r : R} {x : ↥I}, r • ↑x = r * ↑x
-- Init.Data.Option.Lemmas
Option.map_if : ∀ {α : Type u_1} {β : Type u_2} {c : Prop} {a : α} {f : α → β} {x : Decidable c},
  Option.map f (if c then some a else none) = if c then some (f a) else none
-- Mathlib.Algebra.GroupWithZero.Basic
/-- An element of a right-cancellative `MulZeroOneClass` fixed by left multiplication by
an element other than one must be zero.  -/
eq_zero_of_mul_eq_self_left : ∀ {M₀ : Type u_1} {a b : M₀} [inst : MulZeroOneClass M₀] [IsRightCancelMulZero M₀], b ≠ 1 → b * a = a → a = 0
-- Mathlib.Data.Set.Pairwise.Basic
/-- If the range of `f` is pairwise disjoint, then the image of any set `s` under `f` is as well.  -/
Pairwise.pairwiseDisjoint : ∀ {α : Type u_1} {ι : Type u_4} [inst : PartialOrder α] [inst_1 : OrderBot α] {f : ι → α},
  Pairwise (Function.onFun Disjoint f) → ∀ (s : Set ι), s.PairwiseDisjoint f
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.MonoOver.instBot : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.Limits.HasInitial C] →
      [CategoryTheory.Limits.InitialMonoClass C] → {X : C} → Bot (CategoryTheory.MonoOver X)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryCofan.map_inl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {F : CategoryTheory.Functor C D} {X Y : C} (s : CategoryTheory.Limits.BinaryCofan X Y),
  (CategoryTheory.Limits.BinaryCofan.map F s).inl = F.map s.inl
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
_private.Mathlib.RingTheory.MvPowerSeries.Evaluation.0.MvPowerSeries.instUniformSpaceMvPolynomial : {σ : Type u_1} → {R : Type u_2} → [inst : CommRing R] → [UniformSpace R] → UniformSpace (MvPolynomial σ R)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.performRatAdd.eq_1 : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
  (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)
  (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (rupHints : Array ℕ)
  (ratHints : Array (ℕ × Array ℕ)),
  f.performRatAdd c pivot rupHints ratHints =
    if f.ratHintsExhaustive pivot ratHints = true then
      have negC := c.negate;
      match f.insertRupUnits negC with
      | (f, contradictionFound) =>
        if contradictionFound = true then (f, false)
        else
          match f.performRupCheck rupHints with
          | (f, derivedLits, derivedEmpty, encounteredError) =>
            if encounteredError = true then (f, false)
            else
              if derivedEmpty = true then (f, false)
              else
                have fold_fn := fun x ratHint =>
                  match x with
                  | (f, allChecksPassed) =>
                    if allChecksPassed = true then f.performRatCheck pivot.negate ratHint else (f, false);
                match Array.foldl fold_fn (f, true) ratHints with
                | (f, allChecksPassed) =>
                  if (!allChecksPassed) = true then (f, false)
                  else
                    match f with
                    | { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments } =>
                      have assignments :=
                        Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.restoreAssignments assignments derivedLits;
                      have f :=
                        { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits,
                            assignments := assignments }.clearRupUnits;
                      (f.insert c, true)
    else (f, false)
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.snd_apply : ∀ (M : Type u_1) (α : Type u_2) (β : Type u_3) [inst : VAdd M α] [inst_1 : VAdd M β],
  ⇑(AddActionHom.snd M α β) = Prod.snd
-- Lean.Elab.App
_private.Lean.Elab.App.0.Lean.Elab.Term.elabAppFnResolutions.toName : List Lean.Syntax → Lean.Name
-- Init.Data.UInt.Lemmas
UInt32.toUSize_toUInt8 : ∀ (n : UInt32), n.toUInt8.toUSize = n.toUSize % 256
-- Init.Data.Nat.Basic
Nat.beq.eq_4 : ∀ (n m : ℕ), n.succ.beq m.succ = n.beq m
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- String description of this measure  -/
Lean.Elab.WF.GuessLex.BasicMeasure.toString : Lean.Elab.WF.GuessLex.BasicMeasure → Lean.MetaM String
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.face_lower : ∀ {n : ℕ} (I : BoxIntegral.Box (Fin (n + 1))) (i : Fin (n + 1)) (a : Fin n),
  (I.face i).lower a = I.lower (i.succAbove a)
-- Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
/-- If `p` does not divide `exponent θ`, then the prime ideals above `p` in `K` are in bijection
with the monic irreducible factors of `minpoly ℤ θ` modulo `p`.
 -/
NumberField.Ideal.primesOverSpanEquivMonicFactorsMod : {K : Type u_1} →
  [inst : Field K] →
    {θ : NumberField.RingOfIntegers K} →
      {p : ℕ} →
        [inst_1 : Fact (Nat.Prime p)] →
          [NumberField K] →
            ¬p ∣ RingOfIntegers.exponent θ →
              ↑((Ideal.span {↑p}).primesOver (NumberField.RingOfIntegers K)) ≃ ↥(RingOfIntegers.monicFactorsMod θ p)
-- Mathlib.Topology.Algebra.Group.Basic
tendsto_neg_nhdsLE_neg : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : AddCommGroup H] [inst_2 : PartialOrder H] [IsOrderedAddMonoid H]
  [ContinuousNeg H] {a : H}, Filter.Tendsto Neg.neg (nhdsWithin (-a) (Set.Iic (-a))) (nhdsWithin a (Set.Ici a))
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
/-- The projection mapping everything that satisfies `J i` to itself, and everything else to `false`
 -/
Profinite.NobelingProof.Proj : {I : Type u} → (J : I → Prop) → [(i : I) → Decidable (J i)] → (I → Bool) → I → Bool
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_map_polynomial : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (q : Polynomial R)
  (f : R → R) (a : A),
  autoParam (p a) cfc_map_polynomial._auto_1 →
    autoParam (ContinuousOn f (spectrum R a)) cfc_map_polynomial._auto_3 →
      cfc (fun x => Polynomial.eval (f x) q) a = (Polynomial.aeval (cfc f a)) q
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
iteratedDerivWithin_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜}, iteratedDerivWithin 0 f s = f
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
Geometry.SimplicialComplex.mem_vertices : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {K : Geometry.SimplicialComplex 𝕜 E} {x : E}, x ∈ K.vertices ↔ {x} ∈ K.faces
-- Mathlib.RingTheory.Localization.LocalizationLocalization
IsFractionRing.isFractionRing_of_isDomain_of_isLocalization : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) [IsDomain R] (S : Type u_2) (T : Type u_3) [inst_2 : CommRing S]
  [inst_3 : CommRing T] [inst_4 : Algebra R S] [inst_5 : Algebra R T] [inst_6 : Algebra S T] [IsScalarTower R S T]
  [IsLocalization M S] [IsFractionRing R T], IsFractionRing S T
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
DirichletCharacter.IsPrimitive.eq_1 : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n), χ.IsPrimitive = (χ.conductor = n)
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Partial.sSupFun.congr_simp : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R}
  {c c_1 : Set (HahnEmbedding.Partial seed)} (e_c : c = c_1) (hc : DirectedOn (fun x1 x2 => x1 ≤ x2) c),
  HahnEmbedding.Partial.sSupFun hc = HahnEmbedding.Partial.sSupFun ⋯
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
le_of_forall_pos_lt_add : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LinearOrder α] [AddLeftMono α] {a b : α},
  (∀ (ε : α), 0 < ε → a < b + ε) → a ≤ b
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Inner
AEMeasurable.inner : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {m : MeasurableSpace α} [inst_3 : MeasurableSpace E] [OpensMeasurableSpace E]
  [SecondCountableTopology E] {μ : MeasureTheory.Measure α} {f g : α → E},
  AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (fun x => inner 𝕜 (f x) (g x)) μ
-- Mathlib.Algebra.GCDMonoid.Nat
Int.normUnit_eq : ∀ (z : ℤ), normUnit z = if 0 ≤ z then 1 else -1
-- Mathlib.Tactic.NormNum.Core
/-- `norm_num` normalizes numerical expressions in the goal. By default, it supports the operations
`+` `-` `*` `/` `⁻¹` `^` and `%` over types with (at least) an `AddMonoidWithOne` instance, such as
`ℕ`, `ℤ`, `ℚ`, `ℝ`, `ℂ`. In addition to evaluating numerical expressions, `norm_num` will use `simp`
to simplify the goal. If the goal has the form `A = B`, `A ≠ B`, `A < B` or `A ≤ B`, where `A` and
`B` are numerical expressions, `norm_num` will try to close it. It also has a relatively simple
primality prover (available if you import `Mathlib.Tactic.NormNum.Prime`).

This tactic is extensible. Extensions can allow `norm_num` to evaluate more kinds of expressions, or
to prove more kinds of propositions (such as, primality of natural numbers). See the `@[norm_num]`
attribute for further information on extending `norm_num`.

* `norm_num at l` normalizes at location(s) `l`.
* `norm_num [h1, ...]` adds the arguments `h1, ...` to the `simp` set in addition to the default
  `simp` set. All options for `simp` arguments are supported, in particular `←`, `↑` and `↓`.
* `norm_num only` does not use the default `simp` set for simplification. `norm_num only [h1, ...]`
  uses only the arguments `h1, ...` in addition to the routines tagged `@[norm_num]`.
  `norm_num only` still performs post-processing steps, like `simp only`, use `norm_num1` if you
  exclusively want to normalize numerical expressions.
* `norm_num (config := cfg)` uses `cfg` as configuration for `simp` calls (see the `simp` tactic for
  further details).

Examples:
```lean
example : 43 ≤ 74 + (33 : ℤ) := by norm_num
example : ¬ (7-2)/(2*3) ≥ (1:ℝ) + 2/(3^2) := by norm_num
```
 -/
Mathlib.Tactic.normNumConv : Lean.ParserDescr
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_lt_pi_div_two_iff : ∀ {z : ℂ}, z.arg < Real.pi / 2 ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0
-- Mathlib.Data.Rat.Lemmas
Rat.inv_neg : ∀ (q : ℚ), (-q)⁻¹ = -q⁻¹
-- Lean.Elab.RecAppSyntax
_private.Lean.Elab.RecAppSyntax.0.Lean.recAppPosKey : Lean.Name
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.mem_adjoin_iff : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {S : Set E} (x : E),
  x ∈ IntermediateField.adjoin F S ↔ ∃ r s, x = (MvPolynomial.aeval Subtype.val) r / (MvPolynomial.aeval Subtype.val) s
-- Batteries.Data.Fin.Lemmas
Fin.findSomeRev?_zero : ∀ {α : Type u_1} {f : Fin 0 → Option α}, Fin.findSomeRev? f = none
-- Init.Data.SInt.Bitwise
Int8.or_self : ∀ {a : Int8}, a ||| a = a
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.List.forIn'_cons.match_1.eq_1 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.done b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_1 b
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.mul_nonpos_of_nonpos_of_nonneg : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [inst_3 : Std.IsPartialOrder R]
  [Lean.Grind.OrderedRing R] [Std.LawfulOrderLT R] {a b : R}, a ≤ 0 → 0 ≤ b → a * b ≤ 0
-- Mathlib.Topology.Compactness.Paracompact
_private.Mathlib.Topology.Compactness.Paracompact.0.Option.elim'.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (a : α) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match some a with
    | some a => h_1 a
    | none => h_2 ()) =
    h_1 a
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.comp_whiskerRight : ∀ {B : Type u} [self : CategoryTheory.Bicategory B] {a b c : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h) (i : b ⟶ c),
  CategoryTheory.Bicategory.whiskerRight (CategoryTheory.CategoryStruct.comp η θ) i =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η i)
      (CategoryTheory.Bicategory.whiskerRight θ i)
-- Mathlib.RepresentationTheory.Rep.Basic
/-- the underlying type of an object in `Rep k G`  -/
Rep.V : {k : Type u} → {G : Type v} → [inst : Semiring k] → [inst_1 : Monoid G] → Rep.{w, u, v} k G → Type w
-- Mathlib.Algebra.Ring.TransferInstance
/-- Transfer `CommSemiring` across an `Equiv`  -/
Equiv.commSemiring : {α : Type u_1} → {β : Type u_2} → α ≃ β → [CommSemiring β] → CommSemiring α
-- Mathlib.Data.Finset.Max
Finset.isLUB_iff_isGreatest : ∀ {α : Type u_2} [inst : LinearOrder α] (i : α) (s : Finset α), s.Nonempty → (IsLUB (↑s) i ↔ IsGreatest (↑s) i)
-- Mathlib.Data.Finset.Preimage
Finset.sigma_preimage_mk : ∀ {α : Type u} {β : α → Type u_1} [inst : DecidableEq α] (s : Finset ((a : α) × β a)) (t : Finset α),
  (t.sigma fun a => s.preimage (Sigma.mk a) ⋯) = {a ∈ s | a.fst ∈ t}
-- Mathlib.MeasureTheory.Measure.Map
MeasureTheory.mem_ae_map_iff : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {f : α → β},
  AEMeasurable f μ →
    ∀ {s : Set β},
      MeasurableSet s → (s ∈ MeasureTheory.ae (MeasureTheory.Measure.map f μ) ↔ f ⁻¹' s ∈ MeasureTheory.ae μ)
-- Mathlib.Algebra.Lie.DirectSum
/-- The inclusion of each component into a direct sum as a morphism of Lie modules.  -/
DirectSum.lieModuleOf : (R : Type u) →
  (ι : Type v) →
    [inst : CommRing R] →
      (L : Type w₁) →
        (M : ι → Type w) →
          [inst_1 : LieRing L] →
            [inst_2 : (i : ι) → AddCommGroup (M i)] →
              [inst_3 : (i : ι) → Module R (M i)] →
                [inst_4 : (i : ι) → LieRingModule L (M i)] →
                  [DecidableEq ι] → (j : ι) → M j →ₗ⁅R,L⁆ DirectSum ι fun i => M i
-- Mathlib.ModelTheory.Bundled
FirstOrder.Language.Theory.ModelType.mk.injEq : ∀ {L : FirstOrder.Language} {T : L.Theory} (Carrier : Type w) [struc : L.Structure Carrier] [is_model : Carrier ⊨ T]
  [nonempty' : Nonempty Carrier] (Carrier_1 : Type w) (struc_1 : L.Structure Carrier_1) (is_model_1 : Carrier_1 ⊨ T)
  (nonempty'_1 : Nonempty Carrier_1),
  ({ Carrier := Carrier, struc := struc, is_model := is_model, nonempty' := nonempty' } =
      { Carrier := Carrier_1, struc := struc_1, is_model := is_model_1, nonempty' := nonempty'_1 }) =
    (Carrier = Carrier_1 ∧ struc ≍ struc_1)
-- Init.Omega.Int
Lean.Omega.Int.ofNat_le_of_le : ∀ {x y : ℕ}, x ≤ y → ↑x ≤ ↑y
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.IterM.foldM_filterMapWithPostcondition.match_1.eq_1 : ∀ {γ : Type u_1} (motive : Option γ → Sort u_2) (c : γ) (h_1 : (c : γ) → motive (some c))
  (h_2 : (x : Option γ) → motive x),
  (match some c with
    | some c => h_1 c
    | x => h_2 x) =
    h_1 c
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.single_add : ∀ {ι : Type u_2} {β : ι → Type u_4} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddCommGroup (β i)] (p : ENNReal) (i : ι)
  {a b : β i}, PiLp.single p i (a + b) = PiLp.single p i a + PiLp.single p i b
-- Mathlib.LinearAlgebra.Matrix.Transvection
/-- There exist two lists of `TransvectionStruct` such that multiplying by them on the left and
on the right makes a matrix block-diagonal, when the last coefficient is nonzero.  -/
Matrix.Pivot.exists_isTwoBlockDiagonal_of_ne_zero : ∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜),
  M (Sum.inr ()) (Sum.inr ()) ≠ 0 →
    ∃ L L',
      ((List.map Matrix.TransvectionStruct.toMatrix L).prod * M *
          (List.map Matrix.TransvectionStruct.toMatrix L').prod).IsTwoBlockDiagonal
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
ContDiffOn.csinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {s : Set E} {n : WithTop ℕ∞},
  ContDiffOn ℂ n f s → ContDiffOn ℂ n (fun x => Complex.sinh (f x)) s
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.EAdj.symm : ∀ {α : Type u_1} {e f : Set α} {H : Hypergraph α}, H.EAdj e f → H.EAdj f e
-- Mathlib.Order.MinMax
/-- An instance asserting that `min a a = a`  -/
min_idem : ∀ {α : Type u} [inst : LinearOrder α], Std.IdempotentOp min
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Decl.mk.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (toSignature : Lean.Compiler.LCNF.Signature pu)
  (value : Lean.Compiler.LCNF.DeclValue pu) (recursive : Bool) (inlineAttr? : Option Lean.Compiler.InlineAttributeKind),
  sizeOf { toSignature := toSignature, value := value, recursive := recursive, inlineAttr? := inlineAttr? } =
    1 + sizeOf toSignature + sizeOf value + sizeOf recursive + sizeOf inlineAttr?
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- Lax functoriality.  -/
CategoryTheory.Lax.StrongTrans.naturality_comp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} (self : CategoryTheory.Lax.StrongTrans F G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapComp f g))
      (self.naturality (CategoryTheory.CategoryStruct.comp f g)).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (self.app a) (G.map f) (G.map g)).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.naturality f).hom (G.map g))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (self.app b) (G.map g)).hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.naturality g).hom)
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (self.app c)).inv
              (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (self.app c))))))
-- Mathlib.Algebra.Regular.SMul
/-- The element `0` is `M`-regular if and only if `M` is trivial.  -/
IsSMulRegular.subsingleton : ∀ {R : Type u_1} {M : Type u_3} [inst : MonoidWithZero R] [inst_1 : Zero M] [inst_2 : MulActionWithZero R M],
  IsSMulRegular M 0 → Subsingleton M
-- Mathlib.Data.Set.Card
Set.even_ncard_compl_iff : ∀ {α : Type u_1} [Finite α], Even (Nat.card α) → ∀ (s : Set α), Even sᶜ.ncard ↔ Even s.ncard
-- Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
BoundedContinuousFunction.char_mem_charPoly : ∀ {V : Type u_1} {W : Type u_2} [inst : AddCommGroup V] [inst_1 : Module ℝ V] [inst_2 : TopologicalSpace V]
  [inst_3 : AddCommGroup W] [inst_4 : Module ℝ W] [inst_5 : TopologicalSpace W] {e : AddChar ℝ Circle}
  {L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ} {he : Continuous ⇑e} {hL : Continuous fun p => (L p.1) p.2} (w : W),
  BoundedContinuousFunction.char he hL w ∈ BoundedContinuousFunction.charPoly he hL
-- Mathlib.Topology.Inseparable
/-- **Alias** of the reverse direction of `SeparationQuotient.continuous_lift_iff`. -/
SeparationQuotient.continuous_lift : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}
  {hf : ∀ (x y : X), Inseparable x y → f x = f y}, Continuous f → Continuous (SeparationQuotient.lift f hf)
-- Lean.ToExpr
Lean.instToExprISize.mkNat : ℕ → Lean.Expr
-- Mathlib.Lean.Expr.Basic
/-- Traverses an expression `e` and renames bound variables named `old` to `new`.  -/
Lean.Expr.renameBVar : Lean.Expr → Lean.Name → Lean.Name → Lean.Expr
-- Mathlib.GroupTheory.Complement
AddSubgroup.IsComplement.finite_left : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {S : Set G} [H.FiniteIndex],
  AddSubgroup.IsComplement S ↑H → S.Finite
-- Mathlib.Algebra.Notation.Prod
Prod.snd_div : ∀ {G : Type u_8} {H : Type u_9} [inst : Div G] [inst_1 : Div H] (a b : G × H), (a / b).2 = a.2 / b.2
-- Mathlib.Algebra.Free
FreeAddMagma.length.eq_def : ∀ {α : Type u} (x : FreeAddMagma α),
  x.length =
    match x with
    | FreeAddMagma.of _x => 1
    | x.add y => x.length + y.length
-- Mathlib.Lean.Meta.Simp
/-- Construct a `Simp.Context`, following the same algorithm that would be done in a "simp" run:
look up all the simp-lemmas in the library, and adjust (add/erase) as specified by the provided
`simpArgs` list.  -/
Lean.Meta.Simp.Context.ofArgs : Lean.TSyntax `Lean.Parser.Tactic.simpArgs →
  optParam Lean.Meta.Simp.Config { } → Lean.Elab.Tactic.TacticM Lean.Meta.Simp.Context