World: Abbildungen

Stream: new members

[Yagub Aliyev]

https://adam.math.hhu.de/#/g/hhu-adam/robo/world/Function/level/2

It seems that whatever you put instead of g, you always have the same g(x+4)=x+1 in the goal. Why? And what is _root_.f?

example (x : ℤ) : ∃ (g : ℤ → ℤ), (g ∘ f) x = x + 1 := by

let f := fun (x : ℤ) ↦ x - 1
let g := fun (x : ℤ) ↦ x + 2
use g
rw[comp_apply]
unfold _root_.f

[Ruben Van de Velde]

I suppose f is given in the left hand column:

def f (x : ℤ) : ℤ := (x + 4)

[Yagub Aliyev]

So, this doesn't appear in the assumptions but somehow it is an assumption? Interesting! I completed, thank you.

example (x : ℤ) : ∃ (g : ℤ → ℤ), (g ∘ f) x = x + 1 := by

let g := fun (x : ℤ) ↦ x - 3
use g
rw[comp_apply]
unfold _root_.f
ring

[Yagub Aliyev]

Still don't know what is _root_.f

[Ruben Van de Velde]

Where did it come from?

[Yagub Aliyev]

I suppose in my first attempt there were two f functions and therefore Lean tried to distinguish them. It kept working after I erased unnecessary f from the code. It appeared after rw[comp_apply]in the previous attempt.

[Ruben Van de Velde]

Ah, I see what happened. Yeah, lean was disambiguating between the f that the game defines and the one you introduced