Proving from optional parameter

Stream: new members

[Abhimanyu Pallavi Sudhir]

How do I fill in the sorry?

example (c : ℝ) (f : ℝ → ℝ) (g : ℝ → ℝ := λ (x : ℝ), f (2 * c - x)) :  ∀ x, g x = f (2 * c - x) := sorry

Presumably I need to intro and input an x into g somehow -- but how? I know the specific example can be rewritten in a way that makes the proof by assumption, but this situation cropped up in another proof.

[Chris Hughes]

I don't think this is true. The := notation for g, just assigns a default value to g, if the user doesn't specify one when using the lemma, but you still have to prove for any g, since the user can override the default and use whatever value for g they like when using the lemma.

[Kevin Buzzard]

Maybe you want let g := ... in ...?

[Chris Hughes]

If you have let g := something in some proof, you can prove g = something with rfl.