Error during Logical Proofs

Stream: new members

[Praveen Kumar]

example (P Q R : Prop): (P ∧ Q ↔ R ∧ Q) ↔ Q → (P ↔ R) := by
    have ans1  := λ h : (P ∧  Q ↔ R ∧ Q)  => λ hq : Q => iff_intro (λ  hp : P => (h.mp (and_intro hp hq)).left) (λ hr : R => (h.mpr (and_intro hr hq)).left)
have ans2 := λ hq : Q =>  λ hrq : P ↔ R => iff_intro (λ hpq : P ∧  Q => (and_intro (hrq.mp hpq.left) hq)) (λ  hrpq : R ∧ Q => (and_intro (hrq.mpr hrpq.left) hq))
exact iff_intro ans1 ans2

This doesnot seem to work I am getting error :

Line 3, Character 21

application type mismatch
  iff_intro ans1 ans2
argument
  ans2
has type
  Q → (P ↔ R) → (P ∧ Q ↔ R ∧ Q) : Prop
but is expected to have type
  (Q → (P ↔ R)) → (P ∧ Q ↔ R ∧ Q) : Prop

[Praveen Kumar]

Here is the link I posted this in wrong channel meta programming

[Notification Bot]

This topic was moved here from #metaprogramming / tactics > Error during Logical Proofs by Kim Morrison.

[Notification Bot]

A message was moved here from #lean4 > need help with a logical proof by Kim Morrison.

[Aaron Liu]

→ is right associative

[Aaron Liu]

so Q → (P ↔ R) → (P ∧ Q ↔ R ∧ Q) actually means Q → ((P ↔ R) → (P ∧ Q ↔ R ∧ Q))

[Aaron Liu]

which is not the same as (Q → (P ↔ R)) → (P ∧ Q ↔ R ∧ Q), and Lean is complaining about this

[Praveen Kumar]

Oh right I will try to fix it

[Praveen Kumar]

have ans1  := λ h : (P ∧  Q ↔ R ∧ Q)  => λ hq : Q => iff_intro (λ  hp : P => (h.mp (and_intro hp hq)).left) (λ hr : R => (h.mpr (and_intro hr hq)).left)
have ans2 := λ hqpr : Q → (P ↔ R) => iff_intro (λ hpq : P ∧ Q => and_intro ((hqpr hpq.right).mp hpq.left) hpq.right) (λ hrq : R ∧ Q => and_intro ((hqpr hrq.right).mpr hrq.left) hrq.right)
exact iff_intro ans1 ans2