# Zulip Chat Archive

## Stream: new members

### Topic: Eliminating forall in hypothesis and applying.

#### Greg Leo (May 11 2022 at 17:35):

I am working through some simple examples for dealing with real-valued functions in lean. I have two questions.

First, In the following example, how can I apply the introduced variables to eliminate the forall in the hypothesis `rep`

?

Second, once that is eliminated, how can I rewrite, for example, `R x y`

to be `f x >= f y`

using that `rep`

hypothesis?

MWE

```
import tactic
import data.real.basic
open classical set function
section
parameters {A : Type} {R : A → A → Prop}
/- Defininig Complete Relations -/
def complete (R : A → A → Prop) : Prop :=
∀ x y, R x y ∨ R y x
def rtransitive (R : A → A → Prop) : Prop :=
∀ x y z, (R x y ∧ R y z) → R x z
def rational (R : A → A → Prop) : Prop := rtransitive R ∧ complete R
theorem represents : (∃ f : A → ℝ, ∀ x , ∀ y, f x ≥ f y ↔ R x y) → complete R :=
begin
intro h,
{
cases h,
rename [h_w f, h_h rep],
rw [complete],
intro x,
intro y,
sorry,
},
end
end
```

#### Kevin Buzzard (May 11 2022 at 17:36):

Doesn't the `parameter`

give you two `R`

in the definition of `complete`

? I would encourae you to not use parameters; they are not used at all in mathlib for example.

#### Greg Leo (May 11 2022 at 17:37):

That's right. I'm not sure where I picked up this habit, but someone else mentioned it to me as well.

#### Kevin Buzzard (May 11 2022 at 17:39):

Replace `parameters`

with `variables`

would be the first thing I'd do with your code.

#### Greg Leo (May 11 2022 at 17:46):

Ok, this gets those parameters replaced with variables. I will have to read more about the distinction, but I found it here: https://leanprover.github.io/theorem_proving_in_lean/interacting_with_lean.html

```
import tactic
import data.real.basic
open classical set function
section
variables {A : Type}
variables {R : A → A → Prop}
/- Defininig Complete Relations -/
def complete (R : A → A → Prop) : Prop :=
∀ x y, R x y ∨ R y x
def rtransitive (R : A → A → Prop) : Prop :=
∀ x y z, (R x y ∧ R y z) → R x z
def rational (R : A → A → Prop) : Prop := rtransitive R ∧ complete R
theorem represents : (∃ f : A → ℝ, ∀ x , ∀ y, f x ≥ f y ↔ R x y) → complete R :=
begin
intro h,
{
cases h,
rename [h_w f, h_h rep],
rw [complete],
intro x,
intro y,
sorry,
},
end
end
```

#### Greg Leo (May 11 2022 at 17:47):

Hey! That fixed it!

#### Greg Leo (May 11 2022 at 17:48):

```
import tactic
import data.real.basic
open classical set function
section
variables {A : Type}
variables {R : A → A → Prop}
/- Defininig Complete Relations -/
def complete (R : A → A → Prop) : Prop :=
∀ x y, R x y ∨ R y x
def rtransitive (R : A → A → Prop) : Prop :=
∀ x y z, (R x y ∧ R y z) → R x z
def rational (R : A → A → Prop) : Prop := rtransitive R ∧ complete R
theorem represents : (∃ f : A → ℝ, ∀ x , ∀ y, f x ≥ f y ↔ R x y) → complete R :=
begin
intro h,
{
cases h,
rename [h_w f, h_h rep],
rw [complete],
intro x,
intro y,
have rep2 : f x ≥ f y ↔ R x y, from rep x y,
},
end
end
```

#### Greg Leo (May 11 2022 at 17:49):

Let's see if I can make some progress. By the way, @Kevin Buzzard your videos are amazing! I love how fluent you are in Lean. It is inspiring. I find myself emulating the way you talk in the videos when I work with my RA in lean.

#### Kevin Buzzard (May 11 2022 at 17:50):

If you don't like the name `h_w`

(and who would!) then you can do `cases h with f rep`

#### Greg Leo (May 11 2022 at 17:53):

That is better. Making some progress here.

```
import tactic
import data.real.basic
open classical set function
section
variables {A : Type}
variables {R : A → A → Prop}
/- Defininig Complete Relations -/
def complete (R : A → A → Prop) : Prop :=
∀ x y, R x y ∨ R y x
def rtransitive (R : A → A → Prop) : Prop :=
∀ x y z, (R x y ∧ R y z) → R x z
def rational (R : A → A → Prop) : Prop := rtransitive R ∧ complete R
theorem represents : (∃ f : A → ℝ, ∀ x , ∀ y, f x ≥ f y ↔ R x y) → complete R :=
begin
intro h,
{
cases h with f rep,
rw [complete],
intro x,
intro y,
have repxy : f x ≥ f y ↔ R x y, from rep x y,
have repyx : f y ≥ f x ↔ R y x, from rep y x,
cases repxy with fxfyRxy Rxyfxfy,
cases repyx with fyfxRyx Ryxfyfx,
sorry,
},
end
end
```

#### Greg Leo (May 11 2022 at 17:54):

Think I need to show fx >= fy or fy >= fx from completeness of >= on the reals.

Last updated: Dec 20 2023 at 11:08 UTC