## Stream: new members

### Topic: and

#### Thomas Laraia (Jul 11 2021 at 11:51):

How do you take two hypotheses and combine them into one with an ∧?

#### Thomas Laraia (Jul 11 2021 at 12:01):

And taking the other approach, is there a reason the have does not work in the last line?

example (a b : ℕ) : a ∣ b ↔ gcd a b = a :=
begin
split,
intro h,
have j := dvd_refl a,
apply dvd_antisymm,
have d := dvd_gcd_iff a b a,
end


#### Kevin Buzzard (Jul 11 2021 at 12:13):

Thomas Laraia said:

How do you take two hypotheses and combine them into one with an ∧?

You can use the constructor for and, which is called and.intro, or you can just use the pointy brackets "general constructor for a structure" construction:

example (P Q : Prop) (hP : P) (hQ : Q) : P ∧ Q :=
and.intro hP hQ

example (P Q : Prop) (hP : P) (hQ : Q) : P ∧ Q := ⟨hP, hQ⟩


#### Patrick Massot (Jul 11 2021 at 12:15):

Thomas, it will be easier to help you if you provide more context. You should read #mwe. It happens that I recognized an exercise from my tutorials, so I can help you anyway, but it would easier to say so, with a precise reference to the exercise (they are numbered precisely for this purpose).

#### Patrick Massot (Jul 11 2021 at 12:16):

Note also that you don't need the answer to this question to do the exercise (but you'll need to know at some point of course).

#### Patrick Massot (Jul 11 2021 at 12:16):

Let's move to your second question now, the have error.

#### Patrick Massot (Jul 11 2021 at 12:17):

Reading error messages is tricky but very important. The error message says:

function expected at
dvd_gcd_iff
term has type
?m_1 ∣ ?m_2.gcd ?m_3 ↔ ?m_1 ∣ ?m_2 ∧ ?m_1 ∣ ?m_3


#### Patrick Massot (Jul 11 2021 at 12:18):

Lean expect a function here because you ask it to apply dvd_gcd_iffto a, b and a.

#### Patrick Massot (Jul 11 2021 at 12:19):

While dvd_gcd_iff is not a function (here function is meant in the dependent type theory sense, which includes a proof of a forall or imply statement), it's an equivalence.

#### Patrick Massot (Jul 11 2021 at 12:20):

It's an equivalence between statements that feature mysterious ?m_1, ?m_2, ?m_3. It means those are implicit arguments that Lean will try to infer automatically. This is nice from Lean, but the downside is it won't let you provide those arguments explicitly unless you really insist.

#### Patrick Massot (Jul 11 2021 at 12:21):

You can check all this by writing #check dvd_gcd_iff above the exercise.

#### Patrick Massot (Jul 11 2021 at 12:22):

This indeed doesn't show the argument. So you can ask Lean to see them anyway with #check @dvd_gcd_iff

#### Patrick Massot (Jul 11 2021 at 12:22):

Note the curly braces around the argument in the answer (and also when this lemma is explained before the exercise). This is what marks arguments as implicit.

#### Patrick Massot (Jul 11 2021 at 12:24):

This @ trick saying "I want to provide all arguments, please don't try to help" also works inside proofs, so you can fix your last line by using @dvd_gcd_iff there as well. Needless to say, this is not the expected solution. You don't need to know any of this at this stage, but it will become necessary at some point.

#### Patrick Massot (Jul 11 2021 at 12:27):

For something which is half way between the expected solution and your idea, you can try: have d : a ∣ a.gcd b ↔ a ∣ a ∧ a ∣ b := dvd_gcd_iff,. This is give you a proof script that is easier to read and will use the fact that those implicit arguments can be inferred from the statement.

#### Thomas Laraia (Jul 11 2021 at 12:52):

@Patrick Massot Perfect, thank you for the detailed explanation and for linking the minimal working examples page, I'll make sure I do this in the future.

Last updated: Dec 20 2023 at 11:08 UTC