Faster way to proof elementary statements

Stream: new members

[Markus Schmaus]

I'm experimenting with Lean and I find myself often trying to proof involving statements involving ∧ and ∃. These are not hard, but a little tedious. Is there a better, faster way to proof such statements? Here is an example:

import Mathlib

example (x : (ℕ × ℕ)) : (x.1 + x.2 = 4) = ∃ a ≤ 4, ∃ a_1 ≤ 4, ∃ a_2, (a_2 = a_1 ∧ a + a_2 = 4) ∧ x = (a, a_2) := by
  apply propext; apply Iff.intro
  · intros h
    use x.1
    have x1_le := Nat.le_add_left x.2 x.1
    have x2_le := Nat.le_add_right x.1 x.2
    rw [h] at x1_le x2_le
    simp_all only [true_and]
    use x.2
    simp_all only [true_and]
    use x.2
  · intro ⟨_, _, _, _, _, ⟨_, _⟩ , _⟩
    simp_all only

[Damiano Testa]

I'm on mobile, but if you pass as soon as possible the values for the existentials, probably aesop can take care of a lot of the goals?

[Markus Schmaus]

Using aesop on its own fails. I was able to use it to close the subgoals using this:

import Mathlib

example (x : (ℕ × ℕ)) : (x.1 + x.2 = 4) = ∃ a ≤ 4, ∃ a_1 ≤ 4, ∃ a_2, (a_2 = a_1 ∧ a + a_2 = 4) ∧ x = (a, a_2) := by
  have := Nat.le_add_left x.2 x.1
  have := Nat.le_add_right x.1 x.2
  apply propext; apply Iff.intro
  all_goals aesop

Would this be considered good style?

[Kevin Buzzard]

Perhaps style is to a certain extent in the eye of the beholder, but one rule I like is "if the result is mathematically trivial then prove it in as short a space as possible and don't worry about readability because nobody needs to read the proof". So I like your proof :-)