Rewriting in assumption

Stream: new members

[Mukesh Tiwari]

I want to prove this lemma, where F is a Field.

lemma eqor : ∀ (y₁ y₂ : F),
   (y₁ - y₂) * (y₁ + y₂) = 0 → y₁ = y₂ ∨ y₁ = -y₂ :=
   begin
    intros,
    /- I want to multiply (y₁ + y₂)⁻¹ in a
       to y₁ = y₂ -/

   end

and my goal is:

state:
F : Type u_2,
_inst_2 : decidable_eq F,
_inst_4 : field F,
y₁ y₂ : F,
a : (y₁ - y₂) * (y₁ + y₂) = 0
⊢ y₁ = y₂ ∨ y₁ = -y₂

What I want is to multiply (y₁ + y₂)⁻¹ in a to infer (y₁ - y₂) = 0, and similarly, (y₁ + y₂) = 0. How can I do this ?

[Alex J. Best]

lemma eqor {F: Type*} [field F] : ∀ (y₁ y₂ : F),
   (y₁ - y₂) * (y₁ + y₂) = 0 → y₁ = y₂ ∨ y₁ = -y₂ :=
   begin
    intros,
    classical,
    by_cases h : y₁ - y₂ = 0,
    {
      sorry,
    },
    {
      apply_fun ((*) (y₁ - y₂)⁻¹) at a,
      rw [mul_zero, ← mul_assoc, inv_mul_cancel h, one_mul] at a,
      sorry,
    }
   end

[Jalex Stark]

I guess to make this a #mwe you need to add

variables {F : Type}
variables [field F]
variables [decidable_eq F]

?

[Jalex Stark]

Alex, that looks right to me? why did you delete it?

[Alex J. Best]

It was in the wrong order, rewriting

[Mukesh Tiwari]

I deleted nothing, but it was re-formatting (but let me add all the information).

[Alex J. Best]

Maybe there is a way to avoid by cases, but this should work

[Mukesh Tiwari]

I am getting unknown identifier for 'apply_fun'.

[Mukesh Tiwari]

Here is my complete source code (if that helps): https://gist.github.com/mukeshtiwari/23a6256f4edd109f6fe820704bc6aa9c

[Jalex Stark]

Alex should add import tactic to the beginning of their example

[Jalex Stark]

Mukesh, instead of linking your whole source code, you should make a #mwe

[Jalex Stark]

(if you click on the link, the community definition of mwe will appear)

[Bryan Gin-ge Chen]

Here's another proof:

import algebra.field

variables (F : Type*) [field F] -- [decidable_eq F]

lemma eqor : ∀ (y₁ y₂ : F),
   (y₁ - y₂) * (y₁ + y₂) = 0 → y₁ = y₂ ∨ y₁ = -y₂ :=
   begin
    intros,
    rw mul_eq_zero at a,
    cases a,
    { left, rwa [sub_eq_zero] at a, },
    { right, rwa [add_eq_zero_iff_eq_neg] at a, },
    /- I want to multiply (y₁ + y₂)⁻¹ in a
       to y₁ = y₂ -/
   end

[Jalex Stark]

Bryan's proof is nicer, but I guess the answer to Mukesh's original question is apply_fun

[Jalex Stark]

@Mukesh Tiwari , apply_fun is provided by import tactic or if you want to be conservative, import tactic.apply_fun

[Mukesh Tiwari]

Thank you very much every one. I wanted to know how apply (or rewrite in a hypothesis). In Coq, I can simply apply f in H or rewrite H1 in H2. So, both answers are very helpful.

[Bryan Gin-ge Chen]

Yeah, for some reason, the preposition we use in lean is at, not in.

[Jalex Stark]

If you run through the natural number game, you'd probably pick up several of these "Coq translations" pretty quickly

[Jalex Stark]

https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/