Skip to content

Commit

Permalink
chore(Order.RelIso): remove some porting notes (#12786)
Browse files Browse the repository at this point in the history
We get the `CoeFun` through `FunLike` which seems the current idiom. The changes are reducibly defeq to the porting remnants.
  • Loading branch information
mattrobball authored and apnelson1 committed May 12, 2024
1 parent d3a8b3b commit a884ca2
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 16 deletions.
4 changes: 2 additions & 2 deletions Mathlib/Order/Birkhoff.lean
Original file line number Diff line number Diff line change
Expand Up @@ -239,13 +239,13 @@ variable [DecidableEq α]
birkhoffFinset (a ⊔ b) = birkhoffFinset a ∪ birkhoffFinset b := by
dsimp [OrderEmbedding.birkhoffFinset]
rw [birkhoffSet_sup, OrderIso.coe_toOrderEmbedding]
simpa using OrderIso.map_sup _ _ _
simp

@[simp] lemma birkhoffFinset_inf (a b : α) :
birkhoffFinset (a ⊓ b) = birkhoffFinset a ∩ birkhoffFinset b := by
dsimp [OrderEmbedding.birkhoffFinset]
rw [birkhoffSet_inf, OrderIso.coe_toOrderEmbedding]
simpa using OrderIso.map_inf _ _ _
simp

@[simp] lemma birkhoffSet_apply (a : α) :
birkhoffSet a = OrderIso.lowerSetSupIrred a := by
Expand Down
14 changes: 0 additions & 14 deletions Mathlib/Order/RelIso/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -228,11 +228,6 @@ def toRelHom (f : r ↪r s) : r →r s where
instance : Coe (r ↪r s) (r →r s) :=
⟨toRelHom⟩

-- Porting note: removed
-- see Note [function coercion]
-- instance : CoeFun (r ↪r s) fun _ => α → β :=
-- ⟨fun o => o.toEmbedding⟩

-- TODO: define and instantiate a `RelEmbeddingClass` when `EmbeddingLike` is defined
instance : FunLike (r ↪r s) α β where
coe := fun x => x.toFun
Expand Down Expand Up @@ -636,10 +631,6 @@ theorem toEquiv_injective : Injective (toEquiv : r ≃r s → α ≃ β)
instance : CoeOut (r ≃r s) (r ↪r s) :=
⟨toRelEmbedding⟩

-- Porting note: moved to after `RelHomClass` instance and redefined as `DFunLike.coe`
-- instance : CoeFun (r ≃r s) fun _ => α → β :=
-- ⟨fun f => f⟩

-- TODO: define and instantiate a `RelIsoClass` when `EquivLike` is defined
instance : FunLike (r ≃r s) α β where
coe := fun x => x
Expand All @@ -656,11 +647,6 @@ instance : EquivLike (r ≃r s) α β where
right_inv f := f.right_inv
coe_injective' _ _ hf _ := DFunLike.ext' hf

-- Porting note: helper instance
-- see Note [function coercion]
instance : CoeFun (r ≃r s) fun _ => α → β :=
⟨DFunLike.coe⟩

@[simp]
theorem coe_toRelEmbedding (f : r ≃r s) : (f.toRelEmbedding : α → β) = f :=
rfl
Expand Down

0 comments on commit a884ca2

Please sign in to comment.