Stuck proving disjunction

Stream: new members

[JK]

I am stuck on this proof and not sure why. I have the following partial proof:

import Mathlib

example {a b : ℝ} (h1 : a * b = a) (h2 : a * b = b) :
    (a = 0 ∧ b = 0) ∨ (a = 1 ∧ b = 1) := by
   obtain azero | anzero := eq_or_ne a 0
   left
   constructor
   exact azero
   calc
     b = a*b := id (Eq.symm h2)
     _ = 0*b := by rw [azero]
     _ = 0 := by apply zero_mul
   exact
   right

I believe I have proved that when a=0 then the left half of the goal is true. Now I would like to show that when a ≠ 0 the right half of the goal is true. But I get an error saying that "right" is an unknown identifier.

[Aaron Liu]

Why have you written exact on a line by itself?

[Aaron Liu]

It's parsing it as exact right

[JK]

Because the calc block doesn't seem to close the proof

[JK]

ah, ok

[Aaron Liu]

you should write structured proofs like this

import Mathlib

example {a b : ℝ} (h1 : a * b = a) (h2 : a * b = b) :
    (a = 0 ∧ b = 0) ∨ (a = 1 ∧ b = 1) := by
  obtain azero | anzero := eq_or_ne a 0
  · left
    constructor
    · exact azero
    · calc
      b = a*b := id (Eq.symm h2)
      _ = 0*b := by rw [azero]
      _ = 0 := by apply zero_mul
  · right
    sorry

[Aaron Liu]

every time a tactic makes more than one goal, put as many focusing dots as there are goals

[JK]

Yeah, I tried that at first but the dots seemed to mess up the parsing

[Kenny Lau]

that's when you don't line up the columns

[Kenny Lau]

in Lean whitespace is a real thing

[JK]

Yeah, I'm finding that quite annoying at the moment =)

[Kenny Lau]

just line up your columns properly lol

[Kenny Lau]

2 spaces for every new level

[JK]

OK, so I did get the proof to work but had many questions:

import Mathlib

example {a b : ℝ} (h1 : a * b = a) (h2 : a * b = b) :
    (a = 0 ∧ b = 0) ∨ (a = 1 ∧ b = 1) := by
   obtain azero | anzero := eq_or_ne a 0
   . left
     constructor
     . exact azero
     . calc
         b = a*b := id (Eq.symm h2)
         _ = 0*b := by rw [azero]
         _ = 0 := by apply zero_mul
   . right
     have h3 : a*b = a*1 := by
       calc
         a*b = a := h1
         _ = a*1 := by ring
     have bone : b = 1 := mul_left_cancel₀ anzero h3
     have bnzero : b ≠ 0 := ne_zero_of_eq_one bone
     constructor
     . have h4 : a*b = 1*b := by
        calc
          a*b = b := h2
          _ = 1*b := by ring
       apply mul_right_cancel₀ bnzero h4
     . exact bone

(1) it was really inelegant to have to introduce h3 and h4; how could I have applied the right lemmas directly to the existing hypotheses?
(2) Did I need to introduce and prove bnzero in order to apply mul_right_cancel₀ , or could I have used another lemma and allowed Lean to infer directly that cancellation was possible since I had already proved that b=1?
(3) I am glad that I had b=1 so that I could rely on ne_zero_of_eq_one. If instead b=47 what would have been the right approach?

[Kenny Lau]

@JK for you first question: if a hypothesis is not in exactly the right form, use convert:

import Mathlib

example {a b : ℝ} (h1 : a * b = a) (h2 : a * b = b) :
    (a = 0 ∧ b = 0) ∨ (a = 1 ∧ b = 1) := by
   obtain azero | anzero := eq_or_ne a 0
   . left
     constructor
     . exact azero
     . calc
         b = a*b := id (Eq.symm h2)
         _ = 0*b := by rw [azero]
         _ = 0 := by apply zero_mul
   . right
    --  have h3 : a*b = a*1 := by
    --    calc
    --      a*b = a := h1
    --      _ = a*1 := by ring
     have bone : b = 1 := mul_left_cancel₀ anzero (by convert h1; simp)
     have bnzero : b ≠ 0 := ne_zero_of_eq_one bone
     constructor
     . /- have h4 : a*b = 1*b := by
        calc
          a*b = b := h2
          _ = 1*b := by ring -/
       apply mul_right_cancel₀ bnzero (by convert h2; simp)
     . exact bone

[Kenny Lau]

second question: no
third question: norm_num:

import Mathlib

example (b : ℝ) (hb : b = 47) : b ≠ 0 := by
  rw [hb]; norm_num