Math2001 02 Proofs with structure 04 And last problem

Stream: new members

[Bo Qin]

https://hrmacbeth.github.io/math2001/02_Proofs_with_Structure.html#id28

How do I only use ha hc and hb hd?

example {a b : ℝ} (h1 : a * b = a) (h2 : a * b = b) :
    a = 0 ∧ b = 0 ∨ a = 1 ∧ b = 1 := by
  have h1a: a * b - a = 0 := by addarith[h1]
  have h2a: a * b - b = 0 := by addarith[h2]
  have h1b :=
    calc
    a * (b - 1) = a * b - a := by ring
    _ = 0 := by rw [h1a]
  have h2b :=
    calc
    b * (a - 1) = a * b - b := by ring
    _ = 0 := by rw [h2a]
  have h1c := eq_zero_or_eq_zero_of_mul_eq_zero h1b
  have h2c := eq_zero_or_eq_zero_of_mul_eq_zero h2b
  obtain ha | hb := h1c
  obtain hc | hd := h2c
  left
  constructor
  apply ha
  apply hc
  right
  apply hb
  apply hd

math2001_2_4.png

[Notification Bot]

This topic was moved here from #general > Math2001 02 Proofs with structure 04 And last problem by Patrick Massot.

[Kenny Lau]

what do you mean by "only use"?

[metakuntyyy]

Can you please post a MWE, the file doesn't compile as is

[Kevin Buzzard]

#mwe

[Kyle Miller]

@metakuntyyy If someone is making use of a book like The Mechanics of Proof, I don't think we should be asking for MWEs. That gives a really high bar to asking a question, due to the custom tactics.

Anyway, here's a version that works in Mathlib:

import Mathlib

example {a b : ℝ} (h1 : a * b = a) (h2 : a * b = b) :
    a = 0 ∧ b = 0 ∨ a = 1 ∧ b = 1 := by
  have h1a: a * b - a = 0 := by linarith --addarith[h1]
  have h2a: a * b - b = 0 := by linarith --addarith[h2]
  have h1b :=
    calc
    a * (b - 1) = a * b - a := by ring
    _ = 0 := by rw [h1a]
  have h2b :=
    calc
    b * (a - 1) = a * b - b := by ring
    _ = 0 := by rw [h2a]
  have h1c := eq_zero_or_eq_zero_of_mul_eq_zero h1b
  have h2c := eq_zero_or_eq_zero_of_mul_eq_zero h2b
  obtain ha | hb := h1c
  obtain hc | hd := h2c
  left
  constructor
  apply ha
  apply hc
  right
  apply hb
  apply hd

[metakuntyyy]

Ah, now it makes sense why addarith failed for me, apologies from my side.

[metakuntyyy]

I've filled some steps

import Mathlib

example {a b : ℝ} (h1 : a * b = a) (h2 : a * b = b) :
    a = 0 ∧ b = 0 ∨ a = 1 ∧ b = 1 := by
  have h1a: a * b - a = 0 := by linarith --addarith[h1]
  have h2a: a * b - b = 0 := by linarith --addarith[h2]
  have h1b :=
    calc
    a * (b - 1) = a * b - a := by ring
    _ = 0 := by rw [h1a]
  have h2b :=
    calc
    b * (a - 1) = a * b - b := by ring
    _ = 0 := by rw [h2a]
  have h1c := eq_zero_or_eq_zero_of_mul_eq_zero h1b
  have h2c := eq_zero_or_eq_zero_of_mul_eq_zero h2b
  obtain ha | hb := h1c
  obtain hc | hd := h2c
  left
  constructor
  · exact ha
  · exact hc
  · left
    have hb0 : b=0 :=by
      rw[← h2]
      apply mul_eq_zero.mpr _
      left
      exact ha
    exact And.intro ha hb0
  · cases h2c with
    | inl hd =>
      left
      rw[← h1]
      have hab0:  a*b = 0 :=by
        linarith
      exact And.intro hab0 hd
    | inr he =>
      right
      constructor
      have ha2 : (a-1) +1 = 0+1  :=by
        congr
      simp only [sub_add_cancel, zero_add] at ha2
      exact ha2
      have hb2 : (b-1) +1 = 0+1  :=by
        congr
      simp only [sub_add_cancel, zero_add] at hb2
      exact hb2

I don't know if you can use them in your tool or what you have available, but this closes everything except the hard goal.

[metakuntyyy]

Is that useful to you?

[metakuntyyy]

I've also filled the last step, I don't know if you have access to those theorems, or simp, but I've tried it to be as elementary as possible. If you don't have access to it, try to find the best approximation of the theorem that you can have.

[metakuntyyy]

sub_add_cancel says a-b+b=a, it's true since you are in the real numbers.