## Stream: new members

### Topic: Rewriting in assumption

#### Mukesh Tiwari (May 09 2020 at 01:42):

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 (May 09 2020 at 01:49):

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 (May 09 2020 at 01:50):

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

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


?

#### Jalex Stark (May 09 2020 at 01:51):

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

#### Alex J. Best (May 09 2020 at 01:51):

It was in the wrong order, rewriting

#### Mukesh Tiwari (May 09 2020 at 01:52):

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

#### Alex J. Best (May 09 2020 at 01:52):

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

#### Mukesh Tiwari (May 09 2020 at 01:56):

I am getting unknown identifier for 'apply_fun'.

#### Mukesh Tiwari (May 09 2020 at 01:57):

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

#### Jalex Stark (May 09 2020 at 01:57):

Alex should add import tactic to the beginning of their example

#### Jalex Stark (May 09 2020 at 01:58):

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

#### Bryan Gin-ge Chen (May 09 2020 at 01:59):

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 (May 09 2020 at 02:02):

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

#### Jalex Stark (May 09 2020 at 02:02):

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

#### Mukesh Tiwari (May 09 2020 at 02:03):

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 (May 09 2020 at 02:04):

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

#### Jalex Stark (May 09 2020 at 02:06):

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

#### Jalex Stark (May 09 2020 at 02:06):

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

Last updated: May 08 2021 at 10:12 UTC