Loogle!

Result

Found 455 declarations whose name contains "_apply_coe". Of these, only the first 200 are shown.

• Equiv.sumIsLeft_symm_apply_coe 📋 Mathlib.Logic.Equiv.Defs
  {α : Type u_1} {β : Type u_2} (a : α) : ↑(Equiv.sumIsLeft.symm a) = Sum.inl a
• Equiv.sumIsRight_symm_apply_coe 📋 Mathlib.Logic.Equiv.Defs
  {α : Type u_1} {β : Type u_2} (b : β) : ↑(Equiv.sumIsRight.symm b) = Sum.inr b
• Equiv.optionIsSomeEquiv_symm_apply_coe 📋 Mathlib.Logic.Equiv.Option
  (α : Type u_4) (x : α) : ↑((Equiv.optionIsSomeEquiv α).symm x) = some x
• Equiv.optionSubtype_symm_apply_apply_coe 📋 Mathlib.Logic.Equiv.Option
  {α : Type u_1} {β : Type u_2} [DecidableEq β] (x : β) (e : α ≃ { y // y ≠ x }) (a : α) : ↑((Equiv.optionSubtype x).symm e) (some a) = ↑(e a)
• Equiv.subtypeEquivRight_apply_coe 📋 Mathlib.Logic.Equiv.Basic
  {α : Sort u_1} {p q : α → Prop} (e : ∀ (x : α), p x ↔ q x) (a : { a // p a }) : ↑((Equiv.subtypeEquivRight e) a) = ↑a
• Equiv.subtypeEquivRight_symm_apply_coe 📋 Mathlib.Logic.Equiv.Basic
  {α : Sort u_1} {p q : α → Prop} (e : ∀ (x : α), p x ↔ q x) (b : { b // q b }) : ↑((Equiv.subtypeEquivRight e).symm b) = ↑b
• Equiv.sigmaSubtype_symm_apply_coe_fst 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_9} {β : α → Type u_10} (a : α) (b : β a) : (↑((Equiv.sigmaSubtype a).symm b)).fst = a
• Equiv.sigmaSubtype_symm_apply_coe_snd 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_9} {β : α → Type u_10} (a : α) (b : β a) : (↑((Equiv.sigmaSubtype a).symm b)).snd = b
• Equiv.subtypeSubtypeEquivSubtype_apply_coe 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_9} {p q : α → Prop} (h : ∀ {x : α}, q x → p x) (a✝ : { x // q ↑x }) : ↑((Equiv.subtypeSubtypeEquivSubtype h) a✝) = ↑↑a✝
• Equiv.subtypeSubtypeEquivSubtype_symm_apply_coe_coe 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_9} {p q : α → Prop} (h : ∀ {x : α}, q x → p x) (a✝ : Subtype q) : ↑↑((Equiv.subtypeSubtypeEquivSubtype h).symm a✝) = ↑a✝
• Equiv.subtypeSubtypeEquivSubtypeExists_apply_coe 📋 Mathlib.Logic.Equiv.Basic
  {α : Sort u_1} (p : α → Prop) (q : Subtype p → Prop) (a : Subtype q) : ↑((Equiv.subtypeSubtypeEquivSubtypeExists p q) a) = ↑↑a
• Equiv.subtypeSubtypeEquivSubtypeInter_apply_coe 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u} (p q : α → Prop) (a✝ : { x // q ↑x }) : ↑((Equiv.subtypeSubtypeEquivSubtypeInter p q) a✝) = ↑↑a✝
• Equiv.subtypeSubtypeEquivSubtypeInter_symm_apply_coe_coe 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u} (p q : α → Prop) (a✝ : { x // p x ∧ q x }) : ↑↑((Equiv.subtypeSubtypeEquivSubtypeInter p q).symm a✝) = ↑a✝
• Equiv.subtypeSubtypeEquivSubtypeExists_symm_apply_coe_coe 📋 Mathlib.Logic.Equiv.Basic
  {α : Sort u_1} (p : α → Prop) (q : Subtype p → Prop) (a : { a // ∃ (h : p a), q ⟨a, h⟩ }) : ↑↑((Equiv.subtypeSubtypeEquivSubtypeExists p q).symm a) = ↑a
• Equiv.subtypePreimage_symm_apply_coe_pos 📋 Mathlib.Logic.Equiv.Basic
  {α : Sort u_1} {β : Sort u_4} (p : α → Prop) [DecidablePred p] (x₀ : { a // p a } → β) (x : { a // ¬p a } → β) (a : α) (h : p a) : ↑((Equiv.subtypePreimage p x₀).symm x) a = x₀ ⟨a, h⟩
• Equiv.subtypePreimage_symm_apply_coe_neg 📋 Mathlib.Logic.Equiv.Basic
  {α : Sort u_1} {β : Sort u_4} (p : α → Prop) [DecidablePred p] (x₀ : { a // p a } → β) (x : { a // ¬p a } → β) (a : α) (h : ¬p a) : ↑((Equiv.subtypePreimage p x₀).symm x) a = x ⟨a, h⟩
• Equiv.subtypePreimage_symm_apply_coe 📋 Mathlib.Logic.Equiv.Basic
  {α : Sort u_1} {β : Sort u_4} (p : α → Prop) [DecidablePred p] (x₀ : { a // p a } → β) (x : { a // ¬p a } → β) (a : α) : ↑((Equiv.subtypePreimage p x₀).symm x) a = if h : p a then x₀ ⟨a, h⟩ else x ⟨a, h⟩
• unitsEquivProdSubtype_apply_coe 📋 Mathlib.Algebra.Group.Units.Equiv
  (α : Type u_2) [Monoid α] (u : αˣ) : ↑((unitsEquivProdSubtype α) u) = (↑u, ↑u⁻¹)
• Equiv.Perm.ofSubtype_apply_coe 📋 Mathlib.Algebra.Group.End
  {α : Type u_4} {p : α → Prop} [DecidablePred p] (f : Equiv.Perm (Subtype p)) (x : Subtype p) : (Equiv.Perm.ofSubtype f) ↑x = ↑(f x)
• Equiv.Perm.subtypeEquivSubtypePerm_apply_coe 📋 Mathlib.Algebra.Group.End
  {α : Type u_4} (p : α → Prop) [DecidablePred p] (f : Equiv.Perm (Subtype p)) : ↑((Equiv.Perm.subtypeEquivSubtypePerm p) f) = Equiv.Perm.ofSubtype f
• Subtype.impEmbedding_apply_coe 📋 Mathlib.Logic.Embedding.Basic
  {α : Type u_1} (p q : α → Prop) (h : ∀ (x : α), p x → q x) (x : { x // p x }) : ↑((Subtype.impEmbedding p q h) x) = ↑x
• Subtype.orderEmbedding_apply_coe 📋 Mathlib.Order.Hom.Basic
  {α : Type u_2} [Preorder α] {p q : α → Prop} (h : ∀ (a : α), p a → q a) (x : { x // p x }) : ↑((Subtype.orderEmbedding h) x) = ↑x
• OrderHom.dual_apply_coe 📋 Mathlib.Order.Hom.Basic
  {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) (a✝ : αᵒᵈ) : (OrderHom.dual f) a✝ = (⇑OrderDual.toDual ∘ ⇑f ∘ ⇑OrderDual.ofDual) a✝
• OrderHom.dual_symm_apply_coe 📋 Mathlib.Order.Hom.Basic
  {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : αᵒᵈ →o βᵒᵈ) (a✝ : α) : (OrderHom.dual.symm f) a✝ = (⇑OrderDual.ofDual ∘ ⇑f ∘ ⇑OrderDual.toDual) a✝
• WithZero.withZeroUnitsEquiv_symm_apply_coe 📋 Mathlib.Algebra.GroupWithZero.WithZero
  {G : Type u_4} [GroupWithZero G] [DecidablePred fun a => a = 0] (a : Gˣ) : WithZero.withZeroUnitsEquiv.symm ↑a = ↑a
• WithBot.toDual_apply_coe 📋 Mathlib.Order.WithBot
  {α : Type u_1} (a : α) : WithBot.toDual ↑a = ↑(OrderDual.toDual a)
• WithTop.toDual_apply_coe 📋 Mathlib.Order.WithBot
  {α : Type u_1} (a : α) : WithTop.toDual ↑a = ↑(OrderDual.toDual a)
• WithBot.ofDual_apply_coe 📋 Mathlib.Order.WithBot
  {α : Type u_1} (a : αᵒᵈ) : WithBot.ofDual ↑a = ↑(OrderDual.ofDual a)
• WithTop.ofDual_apply_coe 📋 Mathlib.Order.WithBot
  {α : Type u_1} (a : αᵒᵈ) : WithTop.ofDual ↑a = ↑(OrderDual.ofDual a)
• Equiv.withBotSubtypeNe_symm_apply_coe 📋 Mathlib.Order.WithBot
  {α : Type u_1} (x : α) : ↑(Equiv.withBotSubtypeNe.symm x) = ↑x
• Equiv.withTopSubtypeNe_symm_apply_coe 📋 Mathlib.Order.WithBot
  {α : Type u_1} (x : α) : ↑(Equiv.withTopSubtypeNe.symm x) = ↑x
• Equiv.ofLeftInverse_apply_coe 📋 Mathlib.Logic.Equiv.Set
  {α : Sort u_3} {β : Type u_4} (f : α → β) (f_inv : Nonempty α → β → α) (hf : ∀ (h : Nonempty α), Function.LeftInverse (f_inv h) f) (a : α) : ↑((Equiv.ofLeftInverse f f_inv hf) a) = f a
• Equiv.Set.rangeInl_symm_apply_coe 📋 Mathlib.Logic.Equiv.Set
  (α : Type u_3) (β : Type u_4) (x : α) : ↑((Equiv.Set.rangeInl α β).symm x) = Sum.inl x
• Equiv.Set.rangeInr_symm_apply_coe 📋 Mathlib.Logic.Equiv.Set
  (α : Type u_3) (β : Type u_4) (x : β) : ↑((Equiv.Set.rangeInr α β).symm x) = Sum.inr x
• Equiv.Set.univPi_apply_coe 📋 Mathlib.Logic.Equiv.Set
  {α : Type u_3} {β : α → Type u_4} (s : (a : α) → Set (β a)) (f : ↑(Set.univ.pi s)) (a : α) : ↑((Equiv.Set.univPi s) f a) = ↑f a
• Equiv.Set.univPi_symm_apply_coe 📋 Mathlib.Logic.Equiv.Set
  {α : Type u_3} {β : α → Type u_4} (s : (a : α) → Set (β a)) (f : (a : α) → ↑(s a)) (a : α) : ↑((Equiv.Set.univPi s).symm f) a = ↑(f a)
• Equiv.image_apply_coe 📋 Mathlib.Logic.Equiv.Set
  {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s : Set α) (x : ↑s) : ↑((e.image s) x) = e ↑x
• Equiv.Set.rangeSplittingImageEquiv_symm_apply_coe 📋 Mathlib.Logic.Equiv.Set
  {α : Type u_3} {β : Type u_4} (f : α → β) (s : Set ↑(Set.range f)) (x : ↑s) : ↑((Equiv.Set.rangeSplittingImageEquiv f s).symm x) = Set.rangeSplitting f ↑x
• Equiv.Set.rangeSplittingImageEquiv_apply_coe_coe 📋 Mathlib.Logic.Equiv.Set
  {α : Type u_3} {β : Type u_4} (f : α → β) (s : Set ↑(Set.range f)) (x : ↑(Set.rangeSplitting f '' s)) : ↑↑((Equiv.Set.rangeSplittingImageEquiv f s) x) = f ↑x
• Equiv.image_symm_apply_coe 📋 Mathlib.Logic.Equiv.Set
  {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s : Set α) (y : ↑(⇑e '' s)) : ↑((e.image s).symm y) = e.symm ↑y
• unitsEquivNeZero_apply_coe 📋 Mathlib.Algebra.GroupWithZero.Units.Equiv
  {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀ˣ) : ↑(unitsEquivNeZero a) = ↑a
• Nonneg.unitsEquivPos_apply_coe 📋 Mathlib.Algebra.Order.Nonneg.Field
  (R : Type u_2) [DivisionSemiring R] [PartialOrder R] [IsStrictOrderedRing R] [PosMulReflectLT R] (r : { r // 0 ≤ r }ˣ) : ↑((Nonneg.unitsEquivPos R) r) = ↑↑r
• Nonneg.val_unitsEquivPos_symm_apply_coe 📋 Mathlib.Algebra.Order.Nonneg.Field
  (R : Type u_2) [DivisionSemiring R] [PartialOrder R] [IsStrictOrderedRing R] [PosMulReflectLT R] (r : { r // 0 < r }) : ↑↑((Nonneg.unitsEquivPos R).symm r) = ↑r
• Nonneg.val_inv_unitsEquivPos_symm_apply_coe 📋 Mathlib.Algebra.Order.Nonneg.Field
  (R : Type u_2) [DivisionSemiring R] [PartialOrder R] [IsStrictOrderedRing R] [PosMulReflectLT R] (r : { r // 0 < r }) : ↑↑((Nonneg.unitsEquivPos R).symm r)⁻¹ = (↑r)⁻¹
• Equiv.finsetSubtypeComm_apply_coe 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} (p : α → Prop) (s : Finset { a // p a }) : ↑((Equiv.finsetSubtypeComm p) s) = Finset.map { toFun := fun a => ↑a, inj' := ⋯ } s
• finCongr_apply_coe 📋 Mathlib.Data.Fin.SuccPred
  {n m : ℕ} (h : m = n) (k : Fin m) : ↑((finCongr h) k) = ↑k
• finCongr_symm_apply_coe 📋 Mathlib.Data.Fin.SuccPred
  {n m : ℕ} (h : m = n) (k : Fin n) : ↑((finCongr h).symm k) = ↑k
• List.Nodup.getEquiv_apply_coe 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} [DecidableEq α] (l : List α) (H : l.Nodup) (i : Fin l.length) : ↑((List.Nodup.getEquiv l H) i) = l.get i
• OrderIso.finsetSetFinite_apply_coe 📋 Mathlib.Data.Set.Finite.Basic
  {α : Type u} (s : Finset α) : ↑(OrderIso.finsetSetFinite s) = ↑s
• Set.Finite.subtypeEquivToFinset_apply_coe 📋 Mathlib.Data.Set.Finite.Basic
  {α : Type u} {s : Set α} (hs : s.Finite) (a : { a // a ∈ s }) : ↑(hs.subtypeEquivToFinset a) = ↑a
• Set.Finite.subtypeEquivToFinset_symm_apply_coe 📋 Mathlib.Data.Set.Finite.Basic
  {α : Type u} {s : Set α} (hs : s.Finite) (b : { b // b ∈ hs.toFinset }) : ↑(hs.subtypeEquivToFinset.symm b) = ↑b
• AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid_apply_coe 📋 Mathlib.Algebra.Group.Submonoid.Operations
  {M : Type u_1} [AddMonoid M] (x : AddUnits M) : ↑(AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid x) = ↑x
• Submonoid.unitsTypeEquivIsUnitSubmonoid_apply_coe 📋 Mathlib.Algebra.Group.Submonoid.Operations
  {M : Type u_1} [Monoid M] (x : Mˣ) : ↑(Submonoid.unitsTypeEquivIsUnitSubmonoid x) = ↑x
• AddSubmonoid.topEquiv_symm_apply_coe 📋 Mathlib.Algebra.Group.Submonoid.Operations
  {M : Type u_5} [AddZeroClass M] (x : M) : ↑(AddSubmonoid.topEquiv.symm x) = x
• Submonoid.topEquiv_symm_apply_coe 📋 Mathlib.Algebra.Group.Submonoid.Operations
  {M : Type u_5} [MulOneClass M] (x : M) : ↑(Submonoid.topEquiv.symm x) = x
• AddMonoidHom.addSubmonoidMap_apply_coe 📋 Mathlib.Algebra.Group.Submonoid.Operations
  {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (M' : AddSubmonoid M) (x : ↥M') : ↑((f.addSubmonoidMap M') x) = f ↑x
• MonoidHom.submonoidMap_apply_coe 📋 Mathlib.Algebra.Group.Submonoid.Operations
  {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) (M' : Submonoid M) (x : ↥M') : ↑((f.submonoidMap M') x) = f ↑x
• AddMonoidHom.addSubmonoidComap_apply_coe 📋 Mathlib.Algebra.Group.Submonoid.Operations
  {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (N' : AddSubmonoid N) (x : ↥(AddSubmonoid.comap f N')) : ↑((f.addSubmonoidComap N') x) = f ↑x
• MonoidHom.submonoidComap_apply_coe 📋 Mathlib.Algebra.Group.Submonoid.Operations
  {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) (N' : Submonoid N) (x : ↥(Submonoid.comap f N')) : ↑((f.submonoidComap N') x) = f ↑x
• AddSubgroup.topEquiv_symm_apply_coe 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [AddGroup G] (x : G) : ↑(AddSubgroup.topEquiv.symm x) = x
• Subgroup.topEquiv_symm_apply_coe 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] (x : G) : ↑(Subgroup.topEquiv.symm x) = x
• AddMonoidHom.addSubgroupMap_apply_coe 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (H : AddSubgroup G) (x : ↥H.toAddSubmonoid) : ↑((f.addSubgroupMap H) x) = f ↑x
• MonoidHom.subgroupMap_apply_coe 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') (H : Subgroup G) (x : ↥H.toSubmonoid) : ↑((f.subgroupMap H) x) = f ↑x
• AddMonoidHom.addSubgroupComap_apply_coe 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (H' : AddSubgroup G') (x : ↥(AddSubmonoid.comap f H'.toAddSubmonoid)) : ↑((f.addSubgroupComap H') x) = f ↑x
• MonoidHom.subgroupComap_apply_coe 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') (H' : Subgroup G') (x : ↥(Submonoid.comap f H'.toSubmonoid)) : ↑((f.subgroupComap H') x) = f ↑x
• AddSubgroup.addSubgroupOfEquivOfLe_symm_apply_coe_coe 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_7} [AddGroup G] {H K : AddSubgroup G} (h : H ≤ K) (g : ↥H) : ↑↑((AddSubgroup.addSubgroupOfEquivOfLe h).symm g) = ↑g
• Subgroup.subgroupOfEquivOfLe_symm_apply_coe_coe 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_7} [Group G] {H K : Subgroup G} (h : H ≤ K) (g : ↥H) : ↑↑((Subgroup.subgroupOfEquivOfLe h).symm g) = ↑g
• AddSubgroup.addSubgroupOfEquivOfLe_apply_coe 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_7} [AddGroup G] {H K : AddSubgroup G} (h : H ≤ K) (g : ↥(H.addSubgroupOf K)) : ↑((AddSubgroup.addSubgroupOfEquivOfLe h) g) = ↑↑g
• Subgroup.subgroupOfEquivOfLe_apply_coe 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_7} [Group G] {H K : Subgroup G} (h : H ≤ K) (g : ↥(H.subgroupOf K)) : ↑((Subgroup.subgroupOfEquivOfLe h) g) = ↑↑g
• AddSubgroup.MapSubtype.orderIso_apply_coe 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (H' : AddSubgroup ↥H) : ↑((AddSubgroup.MapSubtype.orderIso H) H') = AddSubgroup.map H.subtype H'
• Subgroup.MapSubtype.orderIso_apply_coe 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] (H : Subgroup G) (H' : Subgroup ↥H) : ↑((Subgroup.MapSubtype.orderIso H) H') = Subgroup.map H.subtype H'
• AddSubsemigroup.equivOp_apply_coe 📋 Mathlib.Algebra.Group.Subsemigroup.MulOpposite
  {M : Type u_2} [Add M] (H : AddSubsemigroup M) (a : ↥H) : ↑(H.equivOp a) = AddOpposite.op ↑a
• Subsemigroup.equivOp_apply_coe 📋 Mathlib.Algebra.Group.Subsemigroup.MulOpposite
  {M : Type u_2} [Mul M] (H : Subsemigroup M) (a : ↥H) : ↑(H.equivOp a) = MulOpposite.op ↑a
• AddSubsemigroup.equivOp_symm_apply_coe 📋 Mathlib.Algebra.Group.Subsemigroup.MulOpposite
  {M : Type u_2} [Add M] (H : AddSubsemigroup M) (b : ↥H.op) : ↑(H.equivOp.symm b) = AddOpposite.unop ↑b
• Subsemigroup.equivOp_symm_apply_coe 📋 Mathlib.Algebra.Group.Subsemigroup.MulOpposite
  {M : Type u_2} [Mul M] (H : Subsemigroup M) (b : ↥H.op) : ↑(H.equivOp.symm b) = MulOpposite.unop ↑b
• AddSubmonoid.equivOp_apply_coe 📋 Mathlib.Algebra.Group.Submonoid.MulOpposite
  {M : Type u_2} [AddZeroClass M] (H : AddSubmonoid M) (a : ↥H) : ↑(H.equivOp a) = AddOpposite.op ↑a
• Submonoid.equivOp_apply_coe 📋 Mathlib.Algebra.Group.Submonoid.MulOpposite
  {M : Type u_2} [MulOneClass M] (H : Submonoid M) (a : ↥H) : ↑(H.equivOp a) = MulOpposite.op ↑a
• AddSubmonoid.equivOp_symm_apply_coe 📋 Mathlib.Algebra.Group.Submonoid.MulOpposite
  {M : Type u_2} [AddZeroClass M] (H : AddSubmonoid M) (b : ↥H.op) : ↑(H.equivOp.symm b) = AddOpposite.unop ↑b
• Submonoid.equivOp_symm_apply_coe 📋 Mathlib.Algebra.Group.Submonoid.MulOpposite
  {M : Type u_2} [MulOneClass M] (H : Submonoid M) (b : ↥H.op) : ↑(H.equivOp.symm b) = MulOpposite.unop ↑b
• AddSubgroup.equivOp_apply_coe 📋 Mathlib.Algebra.Group.Subgroup.MulOpposite
  {G : Type u_2} [AddGroup G] (H : AddSubgroup G) (a : ↥H) : ↑(H.equivOp a) = AddOpposite.op ↑a
• Subgroup.equivOp_apply_coe 📋 Mathlib.Algebra.Group.Subgroup.MulOpposite
  {G : Type u_2} [Group G] (H : Subgroup G) (a : ↥H) : ↑(H.equivOp a) = MulOpposite.op ↑a
• AddSubgroup.equivOp_symm_apply_coe 📋 Mathlib.Algebra.Group.Subgroup.MulOpposite
  {G : Type u_2} [AddGroup G] (H : AddSubgroup G) (b : ↥H.op) : ↑(H.equivOp.symm b) = AddOpposite.unop ↑b
• Subgroup.equivOp_symm_apply_coe 📋 Mathlib.Algebra.Group.Subgroup.MulOpposite
  {G : Type u_2} [Group G] (H : Subgroup G) (b : ↥H.op) : ↑(H.equivOp.symm b) = MulOpposite.unop ↑b
• Set.embeddingOfSubset_apply_coe 📋 Mathlib.Logic.Embedding.Set
  {α : Type u_1} (s t : Set α) (h : s ⊆ t) (x : ↑s) : ↑((s.embeddingOfSubset t h) x) = ↑x
• Equiv.restrictPreimageFinset_apply_coe 📋 Mathlib.Data.Finset.Preimage
  {α : Type u} {β : Type v} (e : α ≃ β) (s : Finset β) (a : ↥(s.preimage ⇑e ⋯)) : ↑((e.restrictPreimageFinset s) a) = e ↑a
• Equiv.restrictPreimageFinset_symm_apply_coe 📋 Mathlib.Data.Finset.Preimage
  {α : Type u} {β : Type v} (e : α ≃ β) (s : Finset β) (b : ↥s) : ↑((e.restrictPreimageFinset s).symm b) = e.symm ↑b
• WithBot.subtypeOrderIso_apply_coe 📋 Mathlib.Order.Hom.WithTopBot
  {α : Type u_1} [PartialOrder α] [OrderBot α] [DecidablePred fun x => x = ⊥] (a : { a // a ≠ ⊥ }) : WithBot.subtypeOrderIso ↑a = ↑a
• WithTop.subtypeOrderIso_apply_coe 📋 Mathlib.Order.Hom.WithTopBot
  {α : Type u_1} [PartialOrder α] [OrderTop α] [DecidablePred fun x => x = ⊤] (a : { a // a ≠ ⊤ }) : WithTop.subtypeOrderIso ↑a = ↑a
• AddSubmonoid.centerCongr_apply_coe 📋 Mathlib.GroupTheory.Submonoid.Center
  {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (e : M ≃+ N) (r : ↥(AddSubsemigroup.center M)) : ↑((AddSubmonoid.centerCongr e) r) = e ↑r
• Submonoid.centerCongr_apply_coe 📋 Mathlib.GroupTheory.Submonoid.Center
  {M : Type u_2} {N : Type u_1} [MulOneClass M] [MulOneClass N] (e : M ≃* N) (r : ↥(Subsemigroup.center M)) : ↑((Submonoid.centerCongr e) r) = e ↑r
• AddSubmonoid.centerToAddOpposite_apply_coe 📋 Mathlib.GroupTheory.Submonoid.Center
  {M : Type u_2} [AddZeroClass M] (r : ↥(AddSubsemigroup.center M)) : ↑(AddSubmonoid.centerToAddOpposite r) = AddOpposite.op ↑r
• Submonoid.centerToMulOpposite_apply_coe 📋 Mathlib.GroupTheory.Submonoid.Center
  {M : Type u_2} [MulOneClass M] (r : ↥(Subsemigroup.center M)) : ↑(Submonoid.centerToMulOpposite r) = MulOpposite.op ↑r
• AddSubmonoid.centerCongr_symm_apply_coe 📋 Mathlib.GroupTheory.Submonoid.Center
  {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (e : M ≃+ N) (s : ↥(AddSubsemigroup.center N)) : ↑((AddSubmonoid.centerCongr e).symm s) = e.symm ↑s
• Submonoid.centerCongr_symm_apply_coe 📋 Mathlib.GroupTheory.Submonoid.Center
  {M : Type u_2} {N : Type u_1} [MulOneClass M] [MulOneClass N] (e : M ≃* N) (s : ↥(Subsemigroup.center N)) : ↑((Submonoid.centerCongr e).symm s) = e.symm ↑s
• AddSubsemigroup.centerCongr_apply_coe 📋 Mathlib.GroupTheory.Submonoid.Center
  {M : Type u_2} {N : Type u_1} [Add M] [Add N] (e : M ≃+ N) (r : ↥(AddSubsemigroup.center M)) : ↑((AddSubsemigroup.centerCongr e) r) = e ↑r
• Subsemigroup.centerCongr_apply_coe 📋 Mathlib.GroupTheory.Submonoid.Center
  {M : Type u_2} {N : Type u_1} [Mul M] [Mul N] (e : M ≃* N) (r : ↥(Subsemigroup.center M)) : ↑((Subsemigroup.centerCongr e) r) = e ↑r
• AddSubmonoid.centerToAddOpposite_symm_apply_coe 📋 Mathlib.GroupTheory.Submonoid.Center
  {M : Type u_2} [AddZeroClass M] (r : ↥(AddSubsemigroup.center Mᵃᵒᵖ)) : ↑(AddSubmonoid.centerToAddOpposite.symm r) = AddOpposite.unop ↑r
• Submonoid.centerToMulOpposite_symm_apply_coe 📋 Mathlib.GroupTheory.Submonoid.Center
  {M : Type u_2} [MulOneClass M] (r : ↥(Subsemigroup.center Mᵐᵒᵖ)) : ↑(Submonoid.centerToMulOpposite.symm r) = MulOpposite.unop ↑r
• val_addUnitsCenterToCenterAddUnits_apply_coe 📋 Mathlib.GroupTheory.Submonoid.Center
  (M : Type u_1) [AddMonoid M] (n : AddUnits ↥(AddSubmonoid.center M)) : ↑↑((addUnitsCenterToCenterAddUnits M) n) = ↑↑n
• val_unitsCenterToCenterUnits_apply_coe 📋 Mathlib.GroupTheory.Submonoid.Center
  (M : Type u_1) [Monoid M] (n : (↥(Submonoid.center M))ˣ) : ↑↑((unitsCenterToCenterUnits M) n) = ↑↑n
• AddSubsemigroup.centerCongr_symm_apply_coe 📋 Mathlib.GroupTheory.Submonoid.Center
  {M : Type u_2} {N : Type u_1} [Add M] [Add N] (e : M ≃+ N) (s : ↥(AddSubsemigroup.center N)) : ↑((AddSubsemigroup.centerCongr e).symm s) = e.symm ↑s
• Subsemigroup.centerCongr_symm_apply_coe 📋 Mathlib.GroupTheory.Submonoid.Center
  {M : Type u_2} {N : Type u_1} [Mul M] [Mul N] (e : M ≃* N) (s : ↥(Subsemigroup.center N)) : ↑((Subsemigroup.centerCongr e).symm s) = e.symm ↑s
• AddSubsemigroup.centerToAddOpposite_apply_coe 📋 Mathlib.GroupTheory.Submonoid.Center
  {M : Type u_2} [Add M] (r : ↥(AddSubsemigroup.center M)) : ↑(AddSubsemigroup.centerToAddOpposite r) = AddOpposite.op ↑r
• Subsemigroup.centerToMulOpposite_apply_coe 📋 Mathlib.GroupTheory.Submonoid.Center
  {M : Type u_2} [Mul M] (r : ↥(Subsemigroup.center M)) : ↑(Subsemigroup.centerToMulOpposite r) = MulOpposite.op ↑r
• AddSubsemigroup.centerToAddOpposite_symm_apply_coe 📋 Mathlib.GroupTheory.Submonoid.Center
  {M : Type u_2} [Add M] (r : ↥(AddSubsemigroup.center Mᵃᵒᵖ)) : ↑(AddSubsemigroup.centerToAddOpposite.symm r) = AddOpposite.unop ↑r
• Subsemigroup.centerToMulOpposite_symm_apply_coe 📋 Mathlib.GroupTheory.Submonoid.Center
  {M : Type u_2} [Mul M] (r : ↥(Subsemigroup.center Mᵐᵒᵖ)) : ↑(Subsemigroup.centerToMulOpposite.symm r) = MulOpposite.unop ↑r
• AddSubgroup.centerCongr_apply_coe 📋 Mathlib.GroupTheory.Subgroup.Center
  {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (e : G ≃+ H) (r : ↥(AddSubsemigroup.center G)) : ↑((AddSubgroup.centerCongr e) r) = e ↑r
• Subgroup.centerCongr_apply_coe 📋 Mathlib.GroupTheory.Subgroup.Center
  {G : Type u_1} [Group G] {H : Type u_2} [Group H] (e : G ≃* H) (r : ↥(Subsemigroup.center G)) : ↑((Subgroup.centerCongr e) r) = e ↑r
• AddSubgroup.centerToAddOpposite_apply_coe 📋 Mathlib.GroupTheory.Subgroup.Center
  (G : Type u_1) [AddGroup G] (r : ↥(AddSubsemigroup.center G)) : ↑((AddSubgroup.centerToAddOpposite G) r) = AddOpposite.op ↑r
• Subgroup.centerToMulOpposite_apply_coe 📋 Mathlib.GroupTheory.Subgroup.Center
  (G : Type u_1) [Group G] (r : ↥(Subsemigroup.center G)) : ↑((Subgroup.centerToMulOpposite G) r) = MulOpposite.op ↑r
• AddSubgroup.centerCongr_symm_apply_coe 📋 Mathlib.GroupTheory.Subgroup.Center
  {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (e : G ≃+ H) (s : ↥(AddSubsemigroup.center H)) : ↑((AddSubgroup.centerCongr e).symm s) = e.symm ↑s
• Subgroup.centerCongr_symm_apply_coe 📋 Mathlib.GroupTheory.Subgroup.Center
  {G : Type u_1} [Group G] {H : Type u_2} [Group H] (e : G ≃* H) (s : ↥(Subsemigroup.center H)) : ↑((Subgroup.centerCongr e).symm s) = e.symm ↑s
• AddSubgroup.centerToAddOpposite_symm_apply_coe 📋 Mathlib.GroupTheory.Subgroup.Center
  (G : Type u_1) [AddGroup G] (r : ↥(AddSubsemigroup.center Gᵃᵒᵖ)) : ↑((AddSubgroup.centerToAddOpposite G).symm r) = AddOpposite.unop ↑r
• Subgroup.centerToMulOpposite_symm_apply_coe 📋 Mathlib.GroupTheory.Subgroup.Center
  (G : Type u_1) [Group G] (r : ↥(Subsemigroup.center Gᵐᵒᵖ)) : ↑((Subgroup.centerToMulOpposite G).symm r) = MulOpposite.unop ↑r
• Subgroup.normalizerMonoidHom_apply_apply_coe 📋 Mathlib.GroupTheory.Subgroup.Centralizer
  {G : Type u_1} [Group G] (H : Subgroup G) (x : ↥H.normalizer) (a✝ : ↥H) : ↑((H.normalizerMonoidHom x) a✝) = ↑x * ↑a✝ * (↑x)⁻¹
• Subgroup.normalizerMonoidHom_apply_symm_apply_coe 📋 Mathlib.GroupTheory.Subgroup.Centralizer
  {G : Type u_1} [Group G] (H : Subgroup G) (x : ↥H.normalizer) (a✝ : ↥H) : ↑((MulEquiv.symm (H.normalizerMonoidHom x)) a✝) = (↑x)⁻¹ * ↑a✝ * ↑x
• val_unitsCentralizerEquiv_apply_coe 📋 Mathlib.GroupTheory.GroupAction.ConjAct
  (M : Type u_2) [Monoid M] (x : Mˣ) (a✝ : (↥(Submonoid.centralizer {↑x}))ˣ) : ↑↑((unitsCentralizerEquiv M x) a✝) = ↑↑a✝
• val_unitsCentralizerEquiv_symm_apply_coe 📋 Mathlib.GroupTheory.GroupAction.ConjAct
  (M : Type u_2) [Monoid M] (x : Mˣ) (a✝ : ↥(MulAction.stabilizer (ConjAct Mˣ) x)) : ↑↑((unitsCentralizerEquiv M x).symm a✝) = ↑(ConjAct.ofConjAct ↑a✝)
• Subgroup.equivSMul_apply_coe 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
  {α : Type u_1} {G : Type u_2} [Group G] [Group α] [MulDistribMulAction α G] (a : α) (H : Subgroup G) (x : ↑↑H.toSubmonoid) : ↑((Subgroup.equivSMul a H) x) = a • ↑x
• Subgroup.equivSMul_symm_apply_coe 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
  {α : Type u_1} {G : Type u_2} [Group G] [Group α] [MulDistribMulAction α G] (a : α) (H : Subgroup G) (y : ↑(⇑↑(MulDistribMulAction.toMulEquiv G a) '' ↑H.toSubmonoid)) : ↑((Subgroup.equivSMul a H).symm y) = a⁻¹ • ↑y
• AddSubgroup.orderIsoAddCon_symm_apply_coe 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] (c : AddCon G) : ↑((RelIso.symm AddSubgroup.orderIsoAddCon) c) = c.addSubgroup
• Subgroup.orderIsoCon_symm_apply_coe 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [Group G] (c : Con G) : ↑((RelIso.symm Subgroup.orderIsoCon) c) = c.subgroup
• Submodule.topEquiv_symm_apply_coe 📋 Mathlib.Algebra.Module.Submodule.Lattice
  {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) : ↑(Submodule.topEquiv.symm x) = x
• LinearMap.submoduleComap_apply_coe 📋 Mathlib.Algebra.Module.Submodule.Map
  {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] (f : M →ₗ[R] M₁) (q : Submodule R M₁) (c : ↥(Submodule.comap f q)) : ↑((f.submoduleComap q) c) = f ↑c
• Submodule.comapSubtypeEquivOfLe_apply_coe 📋 Mathlib.Algebra.Module.Submodule.Map
  {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {p q : Submodule R M} (hpq : p ≤ q) (x : ↥(Submodule.comap q.subtype p)) : ↑((Submodule.comapSubtypeEquivOfLe hpq) x) = ↑↑x
• AddHom.codRestrict_apply_coe 📋 Mathlib.Algebra.Group.Subsemigroup.Operations
  {M : Type u_1} {N : Type u_2} {σ : Type u_4} [Add M] [Add N] [SetLike σ N] [AddMemClass σ N] (f : M →ₙ+ N) (S : σ) (h : ∀ (x : M), f x ∈ S) (n : M) : ↑((f.codRestrict S h) n) = f n
• MulHom.codRestrict_apply_coe 📋 Mathlib.Algebra.Group.Subsemigroup.Operations
  {M : Type u_1} {N : Type u_2} {σ : Type u_4} [Mul M] [Mul N] [SetLike σ N] [MulMemClass σ N] (f : M →ₙ* N) (S : σ) (h : ∀ (x : M), f x ∈ S) (n : M) : ↑((f.codRestrict S h) n) = f n
• AddSubsemigroup.topEquiv_symm_apply_coe 📋 Mathlib.Algebra.Group.Subsemigroup.Operations
  {M : Type u_1} [Add M] (x : M) : ↑(AddSubsemigroup.topEquiv.symm x) = x
• Subsemigroup.topEquiv_symm_apply_coe 📋 Mathlib.Algebra.Group.Subsemigroup.Operations
  {M : Type u_1} [Mul M] (x : M) : ↑(Subsemigroup.topEquiv.symm x) = x
• AddHom.subsemigroupMap_apply_coe 📋 Mathlib.Algebra.Group.Subsemigroup.Operations
  {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) (M' : AddSubsemigroup M) (x : ↥M') : ↑((f.subsemigroupMap M') x) = f ↑x
• MulHom.subsemigroupMap_apply_coe 📋 Mathlib.Algebra.Group.Subsemigroup.Operations
  {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (M' : Subsemigroup M) (x : ↥M') : ↑((f.subsemigroupMap M') x) = f ↑x
• AddHom.subsemigroupComap_apply_coe 📋 Mathlib.Algebra.Group.Subsemigroup.Operations
  {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) (N' : AddSubsemigroup N) (x : ↥(AddSubsemigroup.comap f N')) : ↑((f.subsemigroupComap N') x) = f ↑x
• MulHom.subsemigroupComap_apply_coe 📋 Mathlib.Algebra.Group.Subsemigroup.Operations
  {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (N' : Subsemigroup N) (x : ↥(Subsemigroup.comap f N')) : ↑((f.subsemigroupComap N') x) = f ↑x
• AddEquiv.subsemigroupMap_apply_coe 📋 Mathlib.Algebra.Group.Subsemigroup.Operations
  {M : Type u_1} {N : Type u_2} [Add M] [Add N] (e : M ≃+ N) (S : AddSubsemigroup M) (x : ↥S) : ↑((e.subsemigroupMap S) x) = e ↑x
• MulEquiv.subsemigroupMap_apply_coe 📋 Mathlib.Algebra.Group.Subsemigroup.Operations
  {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (e : M ≃* N) (S : Subsemigroup M) (x : ↥S) : ↑((e.subsemigroupMap S) x) = e ↑x
• AddEquiv.subsemigroupMap_symm_apply_coe 📋 Mathlib.Algebra.Group.Subsemigroup.Operations
  {M : Type u_1} {N : Type u_2} [Add M] [Add N] (e : M ≃+ N) (S : AddSubsemigroup M) (x : ↥(AddSubsemigroup.map (↑e) S)) : ↑((e.subsemigroupMap S).symm x) = e.symm ↑x
• MulEquiv.subsemigroupMap_symm_apply_coe 📋 Mathlib.Algebra.Group.Subsemigroup.Operations
  {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (e : M ≃* N) (S : Subsemigroup M) (x : ↥(Subsemigroup.map (↑e) S)) : ↑((e.subsemigroupMap S).symm x) = e.symm ↑x
• NonUnitalSubsemiring.topEquiv_symm_apply_coe 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u} [NonUnitalNonAssocSemiring R] (x : R) : ↑(NonUnitalSubsemiring.topEquiv.symm x) = x
• NonUnitalSubsemiring.centerCongr_apply_coe 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (e : R ≃+* S) (r : ↥(Subsemigroup.center R)) : ↑((NonUnitalSubsemiring.centerCongr e) r) = e ↑r
• RingEquiv.nonUnitalSubsemiringMap_apply_coe 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (e : R ≃+* S) (s : NonUnitalSubsemiring R) (x : ↑↑s.toAddSubmonoid) : ↑((e.nonUnitalSubsemiringMap s) x) = e ↑x
• NonUnitalSubsemiring.centerToMulOpposite_apply_coe 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u} [NonUnitalNonAssocSemiring R] (r : ↥(Subsemigroup.center R)) : ↑(NonUnitalSubsemiring.centerToMulOpposite r) = MulOpposite.op ↑r
• NonUnitalSubsemiring.centerCongr_symm_apply_coe 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (e : R ≃+* S) (s : ↥(Subsemigroup.center S)) : ↑((NonUnitalSubsemiring.centerCongr e).symm s) = (↑e).symm ↑s
• RingEquiv.nonUnitalSubsemiringMap_symm_apply_coe 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (e : R ≃+* S) (s : NonUnitalSubsemiring R) (y : ↑(⇑↑e.toAddEquiv '' ↑s.toAddSubmonoid)) : ↑((e.nonUnitalSubsemiringMap s).symm y) = (↑e).symm ↑y
• NonUnitalSubsemiring.centerToMulOpposite_symm_apply_coe 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u} [NonUnitalNonAssocSemiring R] (r : ↥(Subsemigroup.center Rᵐᵒᵖ)) : ↑(NonUnitalSubsemiring.centerToMulOpposite.symm r) = MulOpposite.unop ↑r
• Subsemiring.topEquiv_symm_apply_coe 📋 Mathlib.Algebra.Ring.Subsemiring.Basic
  {R : Type u} [NonAssocSemiring R] (r : R) : ↑(Subsemiring.topEquiv.symm r) = r
• Subsemiring.centerCongr_apply_coe 📋 Mathlib.Algebra.Ring.Subsemiring.Basic
  {R : Type u} {S : Type v} [NonAssocSemiring R] [NonAssocSemiring S] (e : R ≃+* S) (r : ↥(Subsemigroup.center R)) : ↑((Subsemiring.centerCongr e) r) = e ↑r
• Subsemiring.centerToMulOpposite_apply_coe 📋 Mathlib.Algebra.Ring.Subsemiring.Basic
  {R : Type u} [NonAssocSemiring R] (r : ↥(Subsemigroup.center R)) : ↑(Subsemiring.centerToMulOpposite r) = MulOpposite.op ↑r
• Subsemiring.centerCongr_symm_apply_coe 📋 Mathlib.Algebra.Ring.Subsemiring.Basic
  {R : Type u} {S : Type v} [NonAssocSemiring R] [NonAssocSemiring S] (e : R ≃+* S) (s : ↥(Subsemigroup.center S)) : ↑((Subsemiring.centerCongr e).symm s) = (↑e).symm ↑s
• Subsemiring.centerToMulOpposite_symm_apply_coe 📋 Mathlib.Algebra.Ring.Subsemiring.Basic
  {R : Type u} [NonAssocSemiring R] (r : ↥(Subsemigroup.center Rᵐᵒᵖ)) : ↑(Subsemiring.centerToMulOpposite.symm r) = MulOpposite.unop ↑r
• RingEquiv.subsemiringMap_apply_coe 📋 Mathlib.Algebra.Ring.Subsemiring.Basic
  {R : Type u} {S : Type v} [NonAssocSemiring R] [NonAssocSemiring S] (e : R ≃+* S) (s : Subsemiring R) (x : ↥s) : ↑((e.subsemiringMap s) x) = e ↑x
• RingEquiv.subsemiringMap_symm_apply_coe 📋 Mathlib.Algebra.Ring.Subsemiring.Basic
  {R : Type u} {S : Type v} [NonAssocSemiring R] [NonAssocSemiring S] (e : R ≃+* S) (s : Subsemiring R) (x : ↥(Subsemiring.map e.toRingHom s)) : ↑((e.subsemiringMap s).symm x) = e.symm ↑x
• RingEquiv.restrict_apply_coe 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocSemiring R] [NonAssocSemiring S] {σR : Type u_1} {σS : Type u_2} [SetLike σR R] [SetLike σS S] [SubsemiringClass σR R] [SubsemiringClass σS S] (e : R ≃+* S) (s' : σR) (s : σS) (h : ∀ (x : R), x ∈ s' ↔ e x ∈ s) (a✝ : ↥s') : ↑((e.restrict s' s h) a✝) = e ↑a✝
• RingEquiv.restrict_symm_apply_coe 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocSemiring R] [NonAssocSemiring S] {σR : Type u_1} {σS : Type u_2} [SetLike σR R] [SetLike σS S] [SubsemiringClass σR R] [SubsemiringClass σS S] (e : R ≃+* S) (s' : σR) (s : σS) (h : ∀ (x : R), x ∈ s' ↔ e x ∈ s) (a : ↥s) : ↑((e.restrict s' s h).symm a) = e.symm ↑a
• Subring.topEquiv_symm_apply_coe 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [Ring R] (r : R) : ↑(Subring.topEquiv.symm r) = r
• Subring.centerCongr_apply_coe 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [Ring R] [Ring S] (e : R ≃+* S) (r : ↥(Subsemigroup.center R)) : ↑((Subring.centerCongr e) r) = e ↑r
• Subring.centerToMulOpposite_apply_coe 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [Ring R] (r : ↥(Subsemigroup.center R)) : ↑(Subring.centerToMulOpposite r) = MulOpposite.op ↑r
• Subring.centerCongr_symm_apply_coe 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [Ring R] [Ring S] (e : R ≃+* S) (s : ↥(Subsemigroup.center S)) : ↑((Subring.centerCongr e).symm s) = (↑e).symm ↑s
• Subring.centerToMulOpposite_symm_apply_coe 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [Ring R] (r : ↥(Subsemigroup.center Rᵐᵒᵖ)) : ↑(Subring.centerToMulOpposite.symm r) = MulOpposite.unop ↑r
• AlgEquiv.coe_apply_coe_coe_symm_apply 📋 Mathlib.Algebra.Algebra.Equiv
  {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] {F : Type u_1} [EquivLike F A₁ A₂] [AlgEquivClass F R A₁ A₂] (f : F) (x : A₂) : f ((↑f).symm x) = x
• AlgEquiv.coe_coe_symm_apply_coe_apply 📋 Mathlib.Algebra.Algebra.Equiv
  {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] {F : Type u_1} [EquivLike F A₁ A₂] [AlgEquivClass F R A₁ A₂] (f : F) (x : A₁) : (↑f).symm (f x) = x
• nonZeroDivisorsEquivUnits_symm_apply_coe 📋 Mathlib.Algebra.GroupWithZero.NonZeroDivisors
  {G₀ : Type u_1} [GroupWithZero G₀] (u : G₀ˣ) : ↑(nonZeroDivisorsEquivUnits.symm u) = ↑u
• val_unitsNonZeroDivisorsEquiv_symm_apply_coe 📋 Mathlib.Algebra.GroupWithZero.NonZeroDivisors
  {M₀ : Type u_1} [MonoidWithZero M₀] (u : M₀ˣ) : ↑↑(unitsNonZeroDivisorsEquiv.symm u) = ↑u
• val_inv_unitsNonZeroDivisorsEquiv_symm_apply_coe 📋 Mathlib.Algebra.GroupWithZero.NonZeroDivisors
  {M₀ : Type u_1} [MonoidWithZero M₀] (u : M₀ˣ) : ↑↑(unitsNonZeroDivisorsEquiv.symm u)⁻¹ = ↑u⁻¹
• infIccOrderIsoIccSup_apply_coe 📋 Mathlib.Order.ModularLattice
  {α : Type u_1} [Lattice α] [IsModularLattice α] (a b : α) (x : ↑(Set.Icc (a ⊓ b) a)) : ↑((infIccOrderIsoIccSup a b) x) = ↑x ⊔ b
• infIooOrderIsoIooSup_apply_coe 📋 Mathlib.Order.ModularLattice
  {α : Type u_1} [Lattice α] [IsModularLattice α] (a b : α) (c : ↑(Set.Ioo (a ⊓ b) a)) : ↑((infIooOrderIsoIooSup a b) c) = ↑c ⊔ b
• infIccOrderIsoIccSup_symm_apply_coe 📋 Mathlib.Order.ModularLattice
  {α : Type u_1} [Lattice α] [IsModularLattice α] (a b : α) (x : ↑(Set.Icc b (a ⊔ b))) : ↑((RelIso.symm (infIccOrderIsoIccSup a b)) x) = a ⊓ ↑x
• infIooOrderIsoIooSup_symm_apply_coe 📋 Mathlib.Order.ModularLattice
  {α : Type u_1} [Lattice α] [IsModularLattice α] (a b : α) (c : ↑(Set.Ioo b (a ⊔ b))) : ↑((RelIso.symm (infIooOrderIsoIooSup a b)) c) = a ⊓ ↑c
• Submodule.inclusionSpan_apply_coe 📋 Mathlib.LinearAlgebra.Span.Basic
  {R : Type u_1} {M : Type u_4} (S : Type u_7) [Semiring R] [AddCommMonoid M] [Module R M] [Semiring S] [SMul R S] [Module S M] [IsScalarTower R S M] (p : Submodule R M) (x : ↥p) : ↑((Submodule.inclusionSpan S p) x) = ↑x
• Finsupp.restrictSupportEquiv_symm_apply_coe 📋 Mathlib.Data.Finsupp.Basic
  {α : Type u_1} (s : Set α) (M : Type u_12) [AddCommMonoid M] [DecidablePred fun x => x ∈ s] (f : ↑s →₀ M) : ↑((Finsupp.restrictSupportEquiv s M).symm f) = f.extendDomain
• Finsupp.supportedEquivFinsupp_symm_apply_coe 📋 Mathlib.LinearAlgebra.Finsupp.Supported
  {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) [DecidablePred fun x => x ∈ s] (f : ↑s →₀ M) : ↑((Finsupp.supportedEquivFinsupp s).symm f) = f.extendDomain
• Finsupp.supportedEquivFinsupp_symm_apply_coe_support_val 📋 Mathlib.LinearAlgebra.Finsupp.Supported
  {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) (a✝ : ↑s →₀ M) : (↑((Finsupp.supportedEquivFinsupp s).symm a✝)).support.val = Multiset.map Subtype.val a✝.support.val
• Finsupp.supportedEquivFinsupp_symm_apply_coe_apply 📋 Mathlib.LinearAlgebra.Finsupp.Supported
  {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) (a✝ : ↑s →₀ M) (a : α) : ↑((Finsupp.supportedEquivFinsupp s).symm a✝) a = if h : a ∈ s then a✝ ⟨a, h⟩ else 0
• LinearIndependent.linearCombinationEquiv_apply_coe 📋 Mathlib.LinearAlgebra.LinearIndependent.Defs
  {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) (a✝ : ι →₀ R) : ↑(hv.linearCombinationEquiv a✝) = (Finsupp.linearCombination R v) a✝
• Submodule.fstEquiv_symm_apply_coe 📋 Mathlib.LinearAlgebra.Prod
  (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (m : M) : ↑((Submodule.fstEquiv R M M₂).symm m) = (m, 0)
• Submodule.sndEquiv_symm_apply_coe 📋 Mathlib.LinearAlgebra.Prod
  (R : Type u) (M : Type v) (M₂ : Type w) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (n : M₂) : ↑((Submodule.sndEquiv R M M₂).symm n) = (0, n)
• LinearMap.kerComplementEquivRange_apply_coe 📋 Mathlib.LinearAlgebra.Prod
  {R : Type u_3} {M : Type u_4} {M₂ : Type u_5} [Ring R] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) {C : Submodule R M} (h : IsCompl C f.ker) (a✝ : ↥C) : ↑((f.kerComplementEquivRange h) a✝) = f ↑a✝
• Finset.Nat.antidiagonalEquivFin_symm_apply_coe 📋 Mathlib.Data.Finset.NatAntidiagonal
  (n : ℕ) (x✝ : Fin (n + 1)) : ↑((Finset.Nat.antidiagonalEquivFin n).symm x✝) = (↑x✝, n - ↑x✝)
• Ordinal.enum_symm_apply_coe 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} (r : α → α → Prop) [IsWellOrder α r] (a✝ : α) : ↑((Ordinal.enum r).symm a✝) = (Ordinal.typein r).toRelEmbedding a✝
• Ordinal.ToType.mk_symm_apply_coe 📋 Mathlib.SetTheory.Ordinal.Basic
  {o : Ordinal.{u_1}} (x : o.ToType) : ↑((RelIso.symm Ordinal.ToType.mk) x) = (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding x
• Ordinal.isInitialIso_symm_apply_coe 📋 Mathlib.SetTheory.Cardinal.Aleph
  (x : Cardinal.{u_1}) : ↑((RelIso.symm Ordinal.isInitialIso) x) = x.ord
• DFinsupp.subtypeSupportEqEquiv_apply_coe 📋 Mathlib.Data.DFinsupp.Defs
  {ι : Type u} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] (s : Finset ι) (x✝ : { f // f.support = s }) (i : ↥s) : ↑((DFinsupp.subtypeSupportEqEquiv s) x✝ i) = ↑x✝ ↑i
• DFinsupp.subtypeSupportEqEquiv_symm_apply_coe 📋 Mathlib.Data.DFinsupp.Defs
  {ι : Type u} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] (s : Finset ι) (f : (i : ↥s) → { x // x ≠ 0 }) : ↑((DFinsupp.subtypeSupportEqEquiv s).symm f) = DFinsupp.mk s fun i => ↑(f i)
• Submodule.isIdempotentElemEquiv_apply_coe 📋 Mathlib.LinearAlgebra.Projection
  {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (p : Submodule R E) (f : { f // IsIdempotentElem f ∧ LinearMap.range f = p }) : ↑(p.isIdempotentElemEquiv f) = LinearMap.codRestrict p ↑f ⋯
• Submodule.isIdempotentElemEquiv_symm_apply_coe 📋 Mathlib.LinearAlgebra.Projection
  {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (p : Submodule R E) (f : { f // ∀ (x : ↥p), f ↑x = x }) : ↑(p.isIdempotentElemEquiv.symm f) = p.subtype ∘ₗ ↑f
• Algebra.idealMap_apply_coe 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u_1} [CommSemiring R] (S : Type u_2) [Semiring S] [Algebra R S] (I : Ideal R) (c : ↥I) : ↑((Algebra.idealMap S I) c) = (algebraMap R S) ↑c
• NonUnitalSubring.topEquiv_symm_apply_coe 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} [NonUnitalNonAssocRing R] (x : R) : ↑(NonUnitalSubring.topEquiv.symm x) = x
• NonUnitalSubring.centerCongr_apply_coe 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} [NonUnitalNonAssocRing R] {S : Type u_1} [NonUnitalNonAssocRing S] (e : R ≃+* S) (r : ↥(Subsemigroup.center R)) : ↑((NonUnitalSubring.centerCongr e) r) = e ↑r
• NonUnitalSubring.centerToMulOpposite_apply_coe 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} [NonUnitalNonAssocRing R] (r : ↥(Subsemigroup.center R)) : ↑(NonUnitalSubring.centerToMulOpposite r) = MulOpposite.op ↑r
• NonUnitalSubring.centerCongr_symm_apply_coe 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} [NonUnitalNonAssocRing R] {S : Type u_1} [NonUnitalNonAssocRing S] (e : R ≃+* S) (s : ↥(Subsemigroup.center S)) : ↑((NonUnitalSubring.centerCongr e).symm s) = (↑e).symm ↑s
• NonUnitalSubring.centerToMulOpposite_symm_apply_coe 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {R : Type u} [NonUnitalNonAssocRing R] (r : ↥(Subsemigroup.center Rᵐᵒᵖ)) : ↑(NonUnitalSubring.centerToMulOpposite.symm r) = MulOpposite.unop ↑r
• AlgEquiv.subalgebraMap_apply_coe 📋 Mathlib.Algebra.Algebra.Subalgebra.Basic
  {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (e : A ≃ₐ[R] B) (S : Subalgebra R A) (x : ↑↑S.toAddSubmonoid) : ↑((e.subalgebraMap S) x) = e ↑x
• AlgEquiv.subalgebraMap_symm_apply_coe 📋 Mathlib.Algebra.Algebra.Subalgebra.Basic
  {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (e : A ≃ₐ[R] B) (S : Subalgebra R A) (y : ↑(⇑↑e.toRingEquiv.toAddEquiv '' ↑S.toAddSubmonoid)) : ↑((e.subalgebraMap S).symm y) = (↑↑e).symm ↑y
• Subalgebra.topEquiv_symm_apply_coe 📋 Mathlib.Algebra.Algebra.Subalgebra.Lattice
  {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (a : A) : ↑(Subalgebra.topEquiv.symm a) = a
• skewAdjointPart_apply_coe 📋 Mathlib.Algebra.Star.Module
  (R : Type u_1) {A : Type u_2} [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] (x : A) : ↑((skewAdjointPart R) x) = ⅟2 • (x - star x)
• selfAdjointPart_apply_coe 📋 Mathlib.Algebra.Star.Module
  (R : Type u_1) {A : Type u_2} [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] (x : A) : ↑((selfAdjointPart R) x) = ⅟2 • (x + star x)
• Unitization.inrRangeEquiv_apply_coe 📋 Mathlib.Algebra.Algebra.Unitization
  (R : Type u_1) (A : Type u_2) [CommSemiring R] [StarAddMonoid R] [NonUnitalSemiring A] [Star A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (a : A) : ↑((Unitization.inrRangeEquiv R A) a) = ↑(Unitization.inrNonUnitalStarAlgHom R A) a
• Unitization.val_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe 📋 Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
  (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (x : (PreQuasiregular A)ˣ) : ↑↑((Unitization.unitsFstOne_mulEquiv_quasiregular R).symm x) = 1 + ↑(PreQuasiregular.equiv.symm ↑x)
• Unitization.val_inv_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe 📋 Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
  (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (x : (PreQuasiregular A)ˣ) : ↑(↑((Unitization.unitsFstOne_mulEquiv_quasiregular R).symm x))⁻¹ = 1 + ↑(PreQuasiregular.equiv.symm ↑x⁻¹)
• Algebra.TensorProduct.liftEquiv_symm_apply_coe 📋 Mathlib.RingTheory.TensorProduct.Maps
  {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [Semiring C] [Algebra S C] [Algebra R C] [IsScalarTower R S C] (f' : TensorProduct R A B →ₐ[S] C) : ↑(Algebra.TensorProduct.liftEquiv.symm f') = (f'.comp Algebra.TensorProduct.includeLeft, (AlgHom.restrictScalars R f').comp Algebra.TensorProduct.includeRight)
• Subsemiring.addEquivOp_apply_coe 📋 Mathlib.Algebra.Ring.Subsemiring.MulOpposite
  {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring R) (a : ↥S.toSubmonoid) : ↑(S.addEquivOp a) = MulOpposite.op ↑a

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 6ff4759 serving mathlib revision 519f454