rw side goal proofs

Stream: mathlib4

[Yakov Pechersky]

afaict, rw no longer leaves side goals, so I can't use rw [mul_lt_mul_left] anymore to proceed on a goal and get another side goal. What's the right way to do so?

[Alex J. Best]

Use ?_ in the places you want the goals to be left as side goals perhaps.

[Alex J. Best]

Actually I'm a bit confused, looks like rw does leave side goals for me, at least in simple situations, so I'm not sure whats making it not do so in your situation

[Yakov Pechersky]

Let me look into this again

[Yakov Pechersky]

Hmm -- works for me now in a scratch example. Not sure what happened

[Yakov Pechersky]

Aha, I think I found what I mean:
mathlib3:

import algebra.order.ring.lemmas

variables {α : Type*} [mul_zero_class α] [preorder α] [pos_mul_strict_mono α] [pos_mul_reflect_lt α]

example {b c : α} (h : 0 < c) : c * 0 < c * b ↔ 0 < b :=
begin
  rw [←mul_zero c, mul_lt_mul_left],
--^ c * 0 < c * b ↔ 0 < b
--               ^ c * (c * 0) < c * b ↔ c * 0 < b
--                                ^ 0 < c ONLY
  exact h
end

mathlib4:

class Zero.{u} (α : Type u) where
  zero : α

instance Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
  ofNat := ‹Zero α›.1

variable (M N : Type _) (μ : M → N → N) (r : N → N → Prop) {α : Type _} [Mul α] [Zero α] [LT α] [LE α]

def Covariant : Prop :=
  ∀ (m) {n₁ n₂}, r n₁ n₂ → r (μ m n₁) (μ m n₂)

def Contravariant : Prop :=
  ∀ (m) {n₁ n₂}, r (μ m n₁) (μ m n₂) → r n₁ n₂

class CovariantClass : Prop where
  protected elim : Covariant M N μ r

class ContravariantClass : Prop where
  protected elim : Contravariant M N μ r

section
variable (α)
abbrev PosMulStrictMono  : Prop :=
  CovariantClass { x : α // 0 < x } α (fun x y => x * y) (· < ·)

abbrev PosMulReflectLt : Prop :=
  ContravariantClass { x : α // 0 ≤ x } α (fun x y => x * y) (· < ·)

end

@[simp]
theorem mul_zero : ∀ a : α, a * 0 = 0 := sorry

theorem mul_lt_mul_left [PosMulStrictMono α] [PosMulReflectLt α] (a0 : (0 : α) < a) :
    a * b < a * c ↔ b < c := sorry

theorem zero_lt_mul_left [PosMulStrictMono α] [PosMulReflectLt α] (h : (0 : α) < c) :
  (0 : α) < c * b ↔ 0 < b := by
    rw [←mul_zero c, mul_lt_mul_left]
--  ^ 0 < c * b ↔ 0 < b
--                  ^  c * 0 < c * b ↔ c * 0 < b
--                                  ^ 0 < b ↔ c * 0 < b AND 0 < c
    simp
--  ^ 0 < b ↔ c * 0 < b AND 0 < c
--     ^ 0 < c
    exact h

[Mario Carneiro]

this doesn't seem comparable. The lean 3 proof is showing c * 0 < c * b ↔ 0 < b but the lean 4 proof is 0 < c * b ↔ 0 < b