How do I structure my proof?

Stream: new members

[Bbbbbbbbba]

I'm doing a proof that is going to have more or less the following structure:

import Mathlib

example (a b c : Prop) (d : ℕ → Prop) (long_magic_number : ℕ)
    (ha : a → c) (hb : b → c ∨ d long_magic_number) (hc_with_long_tactic_proof : c → d long_magic_number) (hab : a ∨ b) : ∃n, d n := by
  use long_magic_number
  cases hab with
  | inl h =>
    exact hc_with_long_tactic_proof (ha h)
  | inr h =>
    cases hb h with
    | inl h => exact hc_with_long_tactic_proof h
    | inr h => exact h

However, I don't like this representation because I would need to write down hc_with_long_tactic_proof (standing in for an actual long tactic proof) twice. I know I could do:

example (a b c : Prop) (d : ℕ → Prop) (long_magic_number : ℕ)
    (ha : a → c) (hb : b → c ∨ d long_magic_number) (hc_with_long_tactic_proof : c → d long_magic_number) (hab : a ∨ b) : ∃n, d n := by
  use long_magic_number
  have hc : c → d long_magic_number := by exact hc_with_long_tactic_proof
  cases hab with
  | inl h =>
    exact hc (ha h)
  | inr h =>
    cases hb h with
    | inl h => exact hc h
    | inr h => exact h

But this repeats long_magic_number instead. (Really it is not just a magic number; d long_magic_number stands for some intermediate goal I got after some definition unfolding and intro and use, which has become quite hairy.)

Is there an ideal way I could structure my proof with minimal code duplication?

[Bbbbbbbbba]

I guess I have the "nuclear option" of using by_contra:

import Mathlib

example (a b c : Prop) (d : ℕ → Prop) (long_magic_number : ℕ)
    (ha : a → c) (hb : b → c ∨ d long_magic_number) (hc_with_long_tactic_proof : c → d long_magic_number) (hab : a ∨ b) : ∃n, d n := by
  use long_magic_number
  by_contra h0
  have h1 : c := by
    cases hab with
    | inl h =>
      exact (ha h)
    | inr h =>
      cases hb h with
      | inl h => exact h
      | inr h => contradiction
  exact h0 (hc_with_long_tactic_proof h1)

And I guess if I need to further manipulate my intermediate goal, I could do apply h0 to kinda revert by_contra h0.

[Michal Wallace (tangentstorm)]

It kind of seems like in asking this question, you've hid away the actual problem by using short name. What's preventing you from doing that in the actual code?

[Michal Wallace (tangentstorm)]

Like... I'm tempted to point out that you can give a Prop (or a function to Prop) a name inside a tactic proof:

    let some_prop : Prop := Nat.Prime 4  -- doesn't have to be true
    let param_fact : Nat → Prop := λ n↦ (0 < n)
    have : some_prop → param_fact 5 := by aesop

... But then in your example code, you're already using a short name, so I'm confused. :)

[Bbbbbbbbba]

Michal Wallace (tangentstorm) said:

Like... I'm tempted to point out that you can give a Prop (or a function to Prop) a name inside a tactic proof:

    let some_prop : Prop := Nat.Prime 4  -- doesn't have to be true
    let param_fact : Nat → Prop := λ n↦ (0 < n)
    have : some_prop → param_fact 5 := by aesop

... But then in your example code, you're already using a short name, so I'm confused. :)

Which Prop are you suggesting me give a short name to? Like I said in my question, d long_magic_number stands for some intermediate goal that I have implicitly arrived at through a series of definition unfolding and intro and use, and I don't really want to write it down explicitly even once.

[Bbbbbbbbba]

I did find another option that feels less "nuclear" to me by using if:

import Mathlib

example (a b c : Prop) (d : ℕ → Prop) (long_magic_number : ℕ)
    (ha : a → c) (hb : b → c ∨ d long_magic_number) (hc_with_long_tactic_proof : c → d long_magic_number) (hab : a ∨ b) : ∃n, d n := by
  use long_magic_number
  if hc : c then
    exact hc_with_long_tactic_proof hc
  else
    cases hab with
    | inl h =>
      exact False.elim (hc (ha h))
    | inr h =>
      cases hb h with
      | inl h => exact False.elim (hc h)
      | inr h => exact h