-- Mathlib/NumberTheory/FLT/Four.lean
theorem exists_minimal {a b c : ℤ} (h : Fermat42 a b c) : ∃ a0 b0 c0, Minimal a0 b0 c0

Proof state:
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0

Tactic:
have S_nonempty : S.Nonempty := by
  use Int.natAbs c
  rw [Set.mem_setOf_eq]
  use ⟨a, ⟨b, c⟩⟩

Result:
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
S_nonempty : S.Nonempty
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0

Proof state:
case h
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
⊢ ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ c.natAbs = s.2.2.natAbs

Tactic:
use ⟨a, ⟨b, c⟩⟩

Result:
no goals

Proof state:
case right.h
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
S_nonempty : S.Nonempty
m : ℕ := Nat.find S_nonempty
s0 : ℤ × ℤ × ℤ
hs0 : Fermat42 s0.1 s0.2.1 s0.2.2
hs1 : m = s0.2.2.natAbs
a1 b1 c1 : ℤ
h1 : Fermat42 a1 b1 c1
⊢ c1.natAbs ∈ S

Tactic:
use ⟨a1, ⟨b1, c1⟩⟩

Result:
no goals

Proof state:
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
S_nonempty : S.Nonempty
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0

Tactic:
let m : ℕ := Nat.find S_nonempty

Result:
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
S_nonempty : S.Nonempty
m : ℕ := Nat.find S_nonempty
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0

Proof state:
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
⊢ S.Nonempty

Tactic:
use Int.natAbs c

Result:
case h
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
⊢ c.natAbs ∈ S

Proof state:
case right
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
S_nonempty : S.Nonempty
m : ℕ := Nat.find S_nonempty
s0 : ℤ × ℤ × ℤ
hs0 : Fermat42 s0.1 s0.2.1 s0.2.2
hs1 : m = s0.2.2.natAbs
⊢ ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → s0.2.2.natAbs ≤ c1.natAbs

Tactic:
intro a1 b1 c1 h1

Result:
case right
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
S_nonempty : S.Nonempty
m : ℕ := Nat.find S_nonempty
s0 : ℤ × ℤ × ℤ
hs0 : Fermat42 s0.1 s0.2.1 s0.2.2
hs1 : m = s0.2.2.natAbs
a1 b1 c1 : ℤ
h1 : Fermat42 a1 b1 c1
⊢ s0.2.2.natAbs ≤ c1.natAbs

Proof state:
a b c : ℤ
h : Fermat42 a b c
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0

Tactic:
let S : Set ℕ := { n | ∃ s : ℤ × ℤ × ℤ, Fermat42 s.1 s.2.1 s.2.2 ∧ n = Int.natAbs s.2.2 }

Result:
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0

Proof state:
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
S_nonempty : S.Nonempty
m : ℕ := Nat.find S_nonempty
m_mem : m ∈ S
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0

Tactic:
rcases m_mem with ⟨s0, hs0, hs1⟩

Result:
case intro.intro
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
S_nonempty : S.Nonempty
m : ℕ := Nat.find S_nonempty
s0 : ℤ × ℤ × ℤ
hs0 : Fermat42 s0.1 s0.2.1 s0.2.2
hs1 : m = s0.2.2.natAbs
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0

Proof state:
case intro.intro
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
S_nonempty : S.Nonempty
m : ℕ := Nat.find S_nonempty
s0 : ℤ × ℤ × ℤ
hs0 : Fermat42 s0.1 s0.2.1 s0.2.2
hs1 : m = s0.2.2.natAbs
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0

Tactic:
use s0.1, s0.2.1, s0.2.2, hs0

Result:
case right
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
S_nonempty : S.Nonempty
m : ℕ := Nat.find S_nonempty
s0 : ℤ × ℤ × ℤ
hs0 : Fermat42 s0.1 s0.2.1 s0.2.2
hs1 : m = s0.2.2.natAbs
⊢ ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → s0.2.2.natAbs ≤ c1.natAbs

Proof state:
case right
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
S_nonempty : S.Nonempty
m : ℕ := Nat.find S_nonempty
s0 : ℤ × ℤ × ℤ
hs0 : Fermat42 s0.1 s0.2.1 s0.2.2
hs1 : m = s0.2.2.natAbs
a1 b1 c1 : ℤ
h1 : Fermat42 a1 b1 c1
⊢ m ≤ c1.natAbs

Tactic:
apply Nat.find_min'

Result:
case right.h
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
S_nonempty : S.Nonempty
m : ℕ := Nat.find S_nonempty
s0 : ℤ × ℤ × ℤ
hs0 : Fermat42 s0.1 s0.2.1 s0.2.2
hs1 : m = s0.2.2.natAbs
a1 b1 c1 : ℤ
h1 : Fermat42 a1 b1 c1
⊢ c1.natAbs ∈ S

Proof state:
a b c : ℤ
h : Fermat42 a b c
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0

Tactic:
classical
let S : Set ℕ := { n | ∃ s : ℤ × ℤ × ℤ, Fermat42 s.1 s.2.1 s.2.2 ∧ n = Int.natAbs s.2.2 }
have S_nonempty : S.Nonempty := by
  use Int.natAbs c
  rw [Set.mem_setOf_eq]
  use ⟨a, ⟨b, c⟩⟩
let m : ℕ := Nat.find S_nonempty
have m_mem : m ∈ S := Nat.find_spec S_nonempty
rcases m_mem with ⟨s0, hs0, hs1⟩
use s0.1, s0.2.1, s0.2.2, hs0
intro a1 b1 c1 h1
rw [← hs1]
apply Nat.find_min'
use ⟨a1, ⟨b1, c1⟩⟩

Result:
no goals

Proof state:
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
S_nonempty : S.Nonempty
m : ℕ := Nat.find S_nonempty
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0

Tactic:
have m_mem : m ∈ S := Nat.find_spec S_nonempty

Result:
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
S_nonempty : S.Nonempty
m : ℕ := Nat.find S_nonempty
m_mem : m ∈ S
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0

Proof state:
case h
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
⊢ c.natAbs ∈ S

Tactic:
rw [Set.mem_setOf_eq]

Result:
case h
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
⊢ ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ c.natAbs = s.2.2.natAbs

Proof state:
case right
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
S_nonempty : S.Nonempty
m : ℕ := Nat.find S_nonempty
s0 : ℤ × ℤ × ℤ
hs0 : Fermat42 s0.1 s0.2.1 s0.2.2
hs1 : m = s0.2.2.natAbs
a1 b1 c1 : ℤ
h1 : Fermat42 a1 b1 c1
⊢ s0.2.2.natAbs ≤ c1.natAbs

Tactic:
rw [← hs1]

Result:
case right
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
S_nonempty : S.Nonempty
m : ℕ := Nat.find S_nonempty
s0 : ℤ × ℤ × ℤ
hs0 : Fermat42 s0.1 s0.2.1 s0.2.2
hs1 : m = s0.2.2.natAbs
a1 b1 c1 : ℤ
h1 : Fermat42 a1 b1 c1
⊢ m ≤ c1.natAbs