ゴールに存在量化子が入っている場合、存在量化子がついた変数に値を入ることでゴールの論理式を証明することができます。useタクティクを使うと、「この値を使え」ということができます。例えばこんな感じです。 example : ∃ x : ℝ, 2 < x ∧ x < 3 := by us…