-- Mathlib/Data/Nat/Lattice.lean
theorem sInf_add {n : ℕ} {p : ℕ → Prop} (hn : n ≤ sInf { m | p m }) :
    sInf { m | p (m + n) } + n = sInf { m | p m }

Proof state:
case inr.intro
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
m : ℕ
hm : m ∈ {m | p (m + n)}
hp : ∃ n, n ∈ {m | p m}
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}

Tactic:
rw [Nat.sInf_def ⟨m, hm⟩, Nat.sInf_def hp]

Result:
case inr.intro
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
m : ℕ
hm : m ∈ {m | p (m + n)}
hp : ∃ n, n ∈ {m | p m}
⊢ Nat.find ⋯ + n = Nat.find hp

Proof state:
case inl.inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
hnp : n < sInf {m | p m}
⊢ p (sInf {m | p m} - n + n)

Tactic:
rw [Nat.sub_add_cancel hn]

Result:
case inl.inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
hnp : n < sInf {m | p m}
⊢ p (sInf {m | p m})

Proof state:
case inr.intro
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
m : ℕ
hm : m ∈ {m | p (m + n)}
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}

Tactic:
have hp : ∃ n, n ∈ { m | p m } := ⟨_, hm⟩

Result:
case inr.intro
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
m : ℕ
hm : m ∈ {m | p (m + n)}
hp : ∃ n, n ∈ {m | p m}
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}

Proof state:
case inr.intro
n : ℕ
p : ℕ → Prop
m : ℕ
hm : m ∈ {m | p (m + n)}
hp : ∃ n, n ∈ {m | p m}
hn : n ≤ Nat.find hp
⊢ Nat.find ⋯ + n = Nat.find hp

Tactic:
exact find_add hn

Result:
no goals

Proof state:
case inl
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
⊢ n = sInf {m | p m}

Tactic:
obtain hnp | hnp := hn.eq_or_lt

Result:
case inl.inl
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
hnp : n = sInf {m | p m}
⊢ n = sInf {m | p m}

case inl.inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
hnp : n < sInf {m | p m}
⊢ n = sInf {m | p m}

Proof state:
case inr.intro
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
m : ℕ
hm : m ∈ {m | p (m + n)}
hp : ∃ n, n ∈ {m | p m}
⊢ Nat.find ⋯ + n = Nat.find hp

Tactic:
rw [Nat.sInf_def hp] at hn

Result:
case inr.intro
n : ℕ
p : ℕ → Prop
m : ℕ
hm : m ∈ {m | p (m + n)}
hp : ∃ n, n ∈ {m | p m}
hn : n ≤ Nat.find hp
⊢ Nat.find ⋯ + n = Nat.find hp

Proof state:
case inl
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}

Tactic:
rw [h, Nat.sInf_empty, zero_add]

Result:
case inl
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
⊢ n = sInf {m | p m}

Proof state:
case inl.inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
hnp : n < sInf {m | p m}
⊢ n = sInf {m | p m}

Tactic:
suffices hp : p (sInf { m | p m } - n + n) from (h.subset hp).elim

Result:
case inl.inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
hnp : n < sInf {m | p m}
⊢ p (sInf {m | p m} - n + n)

Proof state:
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}

Tactic:
obtain h | ⟨m, hm⟩ := { m | p (m + n) }.eq_empty_or_nonempty

Result:
case inl
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}

case inr.intro
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
m : ℕ
hm : m ∈ {m | p (m + n)}
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}

Proof state:
case inl.inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
hnp : n < sInf {m | p m}
⊢ p (sInf {m | p m})

Tactic:
exact csInf_mem (nonempty_of_pos_sInf <| n.zero_le.trans_lt hnp)

Result:
no goals

Proof state:
case inl.inl
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
hnp : n = sInf {m | p m}
⊢ n = sInf {m | p m}

Tactic:
exact hnp

Result:
no goals