forall disappearing after the intro

Stream: new members

[V S]

Hello! Say I have the following structure:

import Mathlib

theorem Q: ∀ {n x A B: ℝ}, (n * A = (5 / 7) * n * B) ∧ (x * A = 50 * B) -> (x * A = (7 / 5) * 50 * B)
  intro n x A B h

To start the proof, i use intro, but it messes up the next step I would like to take: I want to say that since forall n (n * A = (5 / 7) * n * B) stands, then (x * A = (5 / 7) * x * B), but am unable to prove it. I think it's due to the intro getting rid of forall. How do I formalize this step?

[Aaron Liu]

You need to put parentheses around the forall

[Aaron Liu]

what you have now is

∀ {n x A B: ℝ}, ((n * A = (5 / 7) * n * B) ∧ (x * A = 50 * B) -> (x * A = (7 / 5) * 50 * B))

[V S]

Aaron Liu said:

what you have now is

∀ {n x A B: ℝ}, ((n * A = (5 / 7) * n * B) ∧ (x * A = 50 * B) -> (x * A = (7 / 5) * 50 * B))

Thank you! But I still don't understand how exactly it would help. I've tried to specify

∀ {n x A B: ℝ}, ((n * A = (5 / 7) * n * B) ∧ (x * A = 50 * B)) -> (x * A = (7 / 5) * 50 * B)

but it doesn't change anything in the proof

[Aaron Liu]

do

(∀ (n A B: ℝ), (n * A = (5 / 7) * n * B) ∧ (x * A = 50 * B)) -> ∀ (x A B: ℝ), (x * A = (7 / 5) * 50 * B)

or maybe

∀ (A B: ℝ), (∀ (n : ℝ), (n * A = (5 / 7) * n * B) ∧ (x * A = 50 * B)) -> ∀ (x : ℝ), (x * A = (7 / 5) * 50 * B)

or maybe something else, depending on what you meant