-- Mathlib/NumberTheory/ClassNumber/Finite.lean
theorem exists_min (I : (Ideal S)⁰) :
    ∃ b ∈ (I : Ideal S),
      b ≠ 0 ∧ ∀ c ∈ (I : Ideal S), abv (Algebra.norm R c) < abv (Algebra.norm R b) → c =
      (0 : S)

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : EuclideanDomain R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
abv : AbsoluteValue R ℤ
I : ↥(Ideal S)⁰
⊢ ∃ b, ∀ (z : ℤ), (fun a => ∃ b ∈ ↑I, b ≠ 0 ∧ abv ((Algebra.norm R) b) = a) z → b ≤ z

Tactic:
use 0

Result:
case h
R : Type u_1
S : Type u_2
inst✝³ : EuclideanDomain R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
abv : AbsoluteValue R ℤ
I : ↥(Ideal S)⁰
⊢ ∀ (z : ℤ), (fun a => ∃ b ∈ ↑I, b ≠ 0 ∧ abv ((Algebra.norm R) b) = a) z → 0 ≤ z

Proof state:
case h
R : Type u_1
S : Type u_2
inst✝³ : EuclideanDomain R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
abv : AbsoluteValue R ℤ
I : ↥(Ideal S)⁰
⊢ ∀ (z : ℤ), (fun a => ∃ b ∈ ↑I, b ≠ 0 ∧ abv ((Algebra.norm R) b) = a) z → 0 ≤ z

Tactic:
rintro _ ⟨b, _, _, rfl⟩

Result:
case h.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝³ : EuclideanDomain R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
abv : AbsoluteValue R ℤ
I : ↥(Ideal S)⁰
b : S
left✝¹ : b ∈ ↑I
left✝ : b ≠ 0
⊢ 0 ≤ abv ((Algebra.norm R) b)

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : EuclideanDomain R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
abv : AbsoluteValue R ℤ
I : ↥(Ideal S)⁰
⊢ ∃ z, (fun a => ∃ b ∈ ↑I, b ≠ 0 ∧ abv ((Algebra.norm R) b) = a) z

Tactic:
obtain ⟨b, b_mem, b_ne_zero⟩ := (I : Ideal S).ne_bot_iff.mp (nonZeroDivisors.coe_ne_zero I)

Result:
case intro.intro
R : Type u_1
S : Type u_2
inst✝³ : EuclideanDomain R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
abv : AbsoluteValue R ℤ
I : ↥(Ideal S)⁰
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
⊢ ∃ z, (fun a => ∃ b ∈ ↑I, b ≠ 0 ∧ abv ((Algebra.norm R) b) = a) z

Proof state:
case intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝³ : EuclideanDomain R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
abv : AbsoluteValue R ℤ
I : ↥(Ideal S)⁰
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
min : ∀ (z : ℤ), (∃ b ∈ ↑I, b ≠ 0 ∧ abv ((Algebra.norm R) b) = z) → abv ((Algebra.norm R) b) ≤ z
⊢ ∃ b ∈ ↑I, b ≠ 0 ∧ ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0

Tactic:
refine ⟨b, b_mem, b_ne_zero, ?_⟩

Result:
case intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝³ : EuclideanDomain R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
abv : AbsoluteValue R ℤ
I : ↥(Ideal S)⁰
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
min : ∀ (z : ℤ), (∃ b ∈ ↑I, b ≠ 0 ∧ abv ((Algebra.norm R) b) = z) → abv ((Algebra.norm R) b) ≤ z
⊢ ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0

Proof state:
case intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝³ : EuclideanDomain R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
abv : AbsoluteValue R ℤ
I : ↥(Ideal S)⁰
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
min : ∀ (z : ℤ), (∃ b ∈ ↑I, b ≠ 0 ∧ abv ((Algebra.norm R) b) = z) → abv ((Algebra.norm R) b) ≤ z
⊢ ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0

Tactic:
intro c hc lt

Result:
case intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝³ : EuclideanDomain R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
abv : AbsoluteValue R ℤ
I : ↥(Ideal S)⁰
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
min : ∀ (z : ℤ), (∃ b ∈ ↑I, b ≠ 0 ∧ abv ((Algebra.norm R) b) = z) → abv ((Algebra.norm R) b) ≤ z
c : S
hc : c ∈ ↑I
lt : abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b)
⊢ c = 0

Proof state:
case intro.intro
R : Type u_1
S : Type u_2
inst✝³ : EuclideanDomain R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
abv : AbsoluteValue R ℤ
I : ↥(Ideal S)⁰
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
⊢ ∃ z, (fun a => ∃ b ∈ ↑I, b ≠ 0 ∧ abv ((Algebra.norm R) b) = a) z

Tactic:
exact ⟨_, ⟨b, b_mem, b_ne_zero, rfl⟩⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝³ : EuclideanDomain R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
abv : AbsoluteValue R ℤ
I : ↥(Ideal S)⁰
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
min : ∀ (z : ℤ), (∃ b ∈ ↑I, b ≠ 0 ∧ abv ((Algebra.norm R) b) = z) → abv ((Algebra.norm R) b) ≤ z
c : S
hc : c ∈ ↑I
c_ne_zero : c ≠ 0
⊢ abv ((Algebra.norm R) b) ≤ abv ((Algebra.norm R) c)

Tactic:
exact min _ ⟨c, hc, c_ne_zero, rfl⟩

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : EuclideanDomain R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
abv : AbsoluteValue R ℤ
I : ↥(Ideal S)⁰
⊢ ∃ b ∈ ↑I, b ≠ 0 ∧ ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0

Tactic:
obtain ⟨_, ⟨b, b_mem, b_ne_zero, rfl⟩, min⟩ := @Int.exists_least_of_bdd
    (fun a => ∃ b ∈ (I : Ideal S), b ≠ (0 : S) ∧ abv (Algebra.norm R b) = a)
  (by
    use 0
    rintro _ ⟨b, _, _, rfl⟩
    apply abv.nonneg)
  (by
    obtain ⟨b, b_mem, b_ne_zero⟩ := (I : Ideal S).ne_bot_iff.mp (nonZeroDivisors.coe_ne_zero I)
    exact ⟨_, ⟨b, b_mem, b_ne_zero, rfl⟩⟩)

Result:
case intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝³ : EuclideanDomain R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
abv : AbsoluteValue R ℤ
I : ↥(Ideal S)⁰
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
min : ∀ (z : ℤ), (∃ b ∈ ↑I, b ≠ 0 ∧ abv ((Algebra.norm R) b) = z) → abv ((Algebra.norm R) b) ≤ z
⊢ ∃ b ∈ ↑I, b ≠ 0 ∧ ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0

Proof state:
case intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝³ : EuclideanDomain R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
abv : AbsoluteValue R ℤ
I : ↥(Ideal S)⁰
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
min : ∀ (z : ℤ), (∃ b ∈ ↑I, b ≠ 0 ∧ abv ((Algebra.norm R) b) = z) → abv ((Algebra.norm R) b) ≤ z
c : S
hc : c ∈ ↑I
lt : abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b)
⊢ c = 0

Tactic:
contrapose! lt with c_ne_zero

Result:
case intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝³ : EuclideanDomain R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
abv : AbsoluteValue R ℤ
I : ↥(Ideal S)⁰
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
min : ∀ (z : ℤ), (∃ b ∈ ↑I, b ≠ 0 ∧ abv ((Algebra.norm R) b) = z) → abv ((Algebra.norm R) b) ≤ z
c : S
hc : c ∈ ↑I
c_ne_zero : c ≠ 0
⊢ abv ((Algebra.norm R) b) ≤ abv ((Algebra.norm R) c)

Proof state:
case h.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝³ : EuclideanDomain R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
abv : AbsoluteValue R ℤ
I : ↥(Ideal S)⁰
b : S
left✝¹ : b ∈ ↑I
left✝ : b ≠ 0
⊢ 0 ≤ abv ((Algebra.norm R) b)

Tactic:
apply abv.nonneg

Result:
no goals