How to use extract_goal result in original proof

Stream: new members

[Alex Gu]

I am trying extract_goal and used it here:

import Mathlib

theorem problem1 (a b c d : ℝ) (h1 : a * b * c - d = 1) (h2 : b * c * d - a = 2) (h3 : c * d * a - b = 3) (h4 : d * a * b - c = -6) : a + b + c + d ≠ 0 := by
  intro h
  have lemma1 : a*b*c + b*c*d + c*d*a + d*a*b = 0 := by
    extract_goal

This gave me this extracted theorem, which I then filled in with linarith:

import Mathlib

theorem extracted_1 (a b c d : ℝ) (h1 : a * b * c - d = 1) (h2 : b * c * d - a = 2) (h3 : c * d * a - b = 3)
  (h4 : d * a * b - c = -6) (h : a + b + c + d = 0) : a * b * c + b * c * d + c * d * a + d * a * b = 0 := by linarith

Now, how can I use this theorem directly in the original proof? This doesn't seem to work, because of some type differences:

import Mathlib

theorem extracted_1 (a b c d : ℝ) (h1 : a * b * c - d = 1) (h2 : b * c * d - a = 2) (h3 : c * d * a - b = 3)
  (h4 : d * a * b - c = -6) (h : a + b + c + d = 0) : a * b * c + b * c * d + c * d * a + d * a * b = 0 := by linarith

theorem problem1 (a b c d : ℝ) (h1 : a * b * c - d = 1) (h2 : b * c * d - a = 2) (h3 : c * d * a - b = 3) (h4 : d * a * b - c = -6) : a + b + c + d ≠ 0 := by
  intro h
  have lemma1 : a*b*c + b*c*d + c*d*a + d*a*b = 0 := by
    exact extracted_1

The error is as follows:

type mismatch
  extracted_1
has type
  ∀ (a b c d : ℝ),
    a * b * c - d = 1 →
      b * c * d - a = 2 →
        c * d * a - b = 3 →
          d * a * b - c = -6 → a + b + c + d = 0 → a * b * c + b * c * d + c * d * a + d * a * b = 0 : Prop
but is expected to have type
  a * b * c + b * c * d + c * d * a + d * a * b = 0 : Prop

[Ruben Van de Velde]

apply, not exact

[Alex Gu]

apply turns it into a bunch of sub-goals, consisting of the hypotheses, but I should be able to prove it directly from the extracted theorem, no?

[Etienne Marion]

You need to fill in the arguments of the theorem.

import Mathlib

theorem extracted_1 (a b c d : ℝ) (h1 : a * b * c - d = 1) (h2 : b * c * d - a = 2) (h3 : c * d * a - b = 3)
  (h4 : d * a * b - c = -6) (h : a + b + c + d = 0) : a * b * c + b * c * d + c * d * a + d * a * b = 0 := by linarith

theorem problem1 (a b c d : ℝ) (h1 : a * b * c - d = 1) (h2 : b * c * d - a = 2) (h3 : c * d * a - b = 3) (h4 : d * a * b - c = -6) : a + b + c + d ≠ 0 := by
  intro h
  have lemma1 : a*b*c + b*c*d + c*d*a + d*a*b = 0 := extracted_1 a b c d h1 h2 h3 h4 h

[Eric Wieser]

extract_goal relies on the pretty-printer, which doesn't round-trip

[Eric Wieser]

set_option pp.all true greatly increases the chance, but doesn't guarantee, that it does so

[Ruben Van de Velde]

Yeah, Eric, but I don't think that's the issue here

[Kevin Buzzard]

Alex Gu said:

The error is as follows:

type mismatch
  extracted_1
has type
  ∀ (a b c d : ℝ),
    a * b * c - d = 1 →
      b * c * d - a = 2 →
        c * d * a - b = 3 →
          d * a * b - c = -6 → a + b + c + d = 0 → a * b * c + b * c * d + c * d * a + d * a * b = 0 : Prop
but is expected to have type
  a * b * c + b * c * d + c * d * a + d * a * b = 0 : Prop

Read and understand the error and you will be able to solve your own problem.

[Kevin Buzzard]

extracted_1 is a function which eats lots of inputs (four numbers and about 5 proofs) and then returns a proof. It is not the proof itself. But it becomes the proof once you have given it the right inputs. Errors are sometimes hard to understand in Lean. But this is an error which you should try and understand because it comes up lots of times and the explanation is pretty helpful on this occasion.

[Michael Rothgang]

Aside: you're nesting your theorems. I had no idea you could even do this - but I think it makes for more readable code if you don't. That is, state your lemmas first and then your main result.