For example, in #934, the following works:
@[to_additive]
theorem mul_sup [CovariantClass α α (· * ·) (· ≤ ·)] (a b c : α) : c * (a ⊔ b) = c * a ⊔ c * b := by
refine' le_antisymm _ _
· rw [← mul_le_mul_iff_left c⁻¹, ← mul_assoc, inv_mul_self, one_mul]
refine sup_le ?_ ?_
· simp only [mul_le_mul_iff_left, le_inv_mul_iff_mul_le, le_sup_left]
· simp only [mul_le_mul_iff_left, le_inv_mul_iff_mul_le, le_sup_right]
· simp only [mul_le_mul_iff_left, sup_le_iff, le_sup_left, le_sup_right, and_self]but replacing any of the simp onlys by plain simp yields errors like
application type mismatch
@Mathlib.Algebra.Order.Group.Defs._auxLemma.5 α AddCommGroup.toAddGroup
argument has type
AddGroup α
but function has type
∀ [inst : Group α] [inst_1 : LE α] [inst_2 : CovariantClass α α (fun x x_1 ↦ x * x_1) fun x x_1 ↦ x ≤ x_1]
{a b c : α}, (b ≤ a⁻¹ * c) = (a * b ≤ c)cc @fpvandoorn
For example, in #934, the following works:
but replacing any of the
simp onlys by plainsimpyields errors likeapplication type mismatch @Mathlib.Algebra.Order.Group.Defs._auxLemma.5 α AddCommGroup.toAddGroup argument has type AddGroup α but function has type ∀ [inst : Group α] [inst_1 : LE α] [inst_2 : CovariantClass α α (fun x x_1 ↦ x * x_1) fun x x_1 ↦ x ≤ x_1] {a b c : α}, (b ≤ a⁻¹ * c) = (a * b ≤ c)cc @fpvandoorn