awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
I : ↥(Ideal S)⁰
obtain :
  ∀ (b : S) (b_mem : b ∈ (↑I : Ideal S)) (b_ne_zero : b ≠ 0)
    (min :
      ∀ (z : ℤ),
        (∃ b ∈ (↑I : Ideal S), b ≠ 0 ∧ (abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) = z) →
          (abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) ≤ z),
    ∃ b ∈ (↑I : Ideal S),
      b ≠ 0 ∧
        ∀ c ∈ (↑I : Ideal S),
          LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) c : R) : ℤ)
              ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ) →
            c = 0
⊢ ∃ b ∈ (↑I : Ideal S),
    b ≠ 0 ∧
      ∀ c ∈ (↑I : Ideal S),
        LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) c : R) : ℤ)
            ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ) →
          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⟩⟩)

Premises used: Int.exists_least_of_bdd, Min.min, rfl
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
I : ↥(Ideal S)⁰
b : S
b_mem : b ∈ (↑I : Ideal S)
b_ne_zero : b ≠ 0
min :
  ∀ (z : ℤ),
    (∃ b ∈ (↑I : Ideal S), b ≠ 0 ∧ (abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) = z) →
      (abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) ≤ z
⊢ ∃ b ∈ (↑I : Ideal S),
    b ≠ 0 ∧
      ∀ c ∈ (↑I : Ideal S),
        LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) c : R) : ℤ)
            ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ) →
          c = 0

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

Premises used: And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
I : ↥(Ideal S)⁰
b : S
b_mem : b ∈ (↑I : Ideal S)
b_ne_zero : b ≠ 0
min :
  ∀ (z : ℤ),
    (∃ b ∈ (↑I : Ideal S), b ≠ 0 ∧ (abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) = z) →
      (abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) ≤ z
refine :
  ∀ c ∈ (↑I : Ideal S),
    LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) c : R) : ℤ)
        ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ) →
      c = 0
⊢ ∃ b ∈ (↑I : Ideal S),
    b ≠ 0 ∧
      ∀ c ∈ (↑I : Ideal S),
        LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) c : R) : ℤ)
            ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ) →
          c = 0

Tactic:
refine ⟨b, b_mem, b_ne_zero, ?_⟩
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
I : ↥(Ideal S)⁰
b : S
b_mem : b ∈ (↑I : Ideal S)
b_ne_zero : b ≠ 0
min :
  ∀ (z : ℤ),
    (∃ b ∈ (↑I : Ideal S), b ≠ 0 ∧ (abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) = z) →
      (abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) ≤ z
c : S
hc : c ∈ (↑I : Ideal S)
lt :
  LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) c : R) : ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)
contrapose! :
  ∀ (c_ne_zero : c ≠ 0),
    LE.le (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) c : R) : ℤ)
⊢ c = 0

Tactic:
contrapose! lt with c_ne_zero
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
I : ↥(Ideal S)⁰
b : S
b_mem : b ∈ (↑I : Ideal S)
b_ne_zero : b ≠ 0
min :
  ∀ (z : ℤ),
    (∃ b ∈ (↑I : Ideal S), b ≠ 0 ∧ (abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) = z) →
      (abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) ≤ z
c : S
hc : c ∈ (↑I : Ideal S)
c_ne_zero : c ≠ 0
⊢ LE.le (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) c : R) : ℤ)

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

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
I : ↥(Ideal S)⁰
b : S
b_mem : b ∈ (↑I : Ideal S)
b_ne_zero : b ≠ 0
min :
  ∀ (z : ℤ),
    (∃ b ∈ (↑I : Ideal S), b ≠ 0 ∧ (abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) = z) →
      (abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) ≤ z
c : S
hc : c ∈ (↑I : Ideal S)
c_ne_zero : c ≠ 0
⊢ LE.le (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) c : R) : ℤ)

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

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
⊢ 0 ∉ finsetApprox bS adm

Tactic:
Finset.notMem_erase _ _

Premises used: Set.Mem, setOf, Finset.notMem_erase
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
x : R
simp :
  (x ≠ 0 ∧
      ∃ (a : Fin (cardM bS adm).succ × Fin (cardM bS adm).succ),
        Membership.mem (γ := Finset (Fin (cardM bS adm).succ × Fin (cardM bS adm).succ)) Finset.univ a ∧
          HSub.hSub (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) a.1 : R)
              ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) a.2 : R) =
            x) ↔
    ∃ (i : Fin (cardM bS adm).succ) (j : Fin (cardM bS adm).succ),
      i ≠ j ∧
        HSub.hSub (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) i : R)
            ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) j : R) =
          x
⊢ x ∈ finsetApprox bS adm ↔
    ∃ (i : Fin (cardM bS adm).succ) (j : Fin (cardM bS adm).succ),
      i ≠ j ∧
        HSub.hSub (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) i : R)
            ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) j : R) =
          x

Tactic:
simp only [finsetApprox, Finset.mem_erase, Finset.mem_image]

Premises used: Finset.mem_image, ClassGroup.finsetApprox, Finset.mem_erase
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
x : R
mp :
  (x ≠ 0 ∧
      ∃ (a : Fin (cardM bS adm).succ × Fin (cardM bS adm).succ),
        Membership.mem (γ := Finset (Fin (cardM bS adm).succ × Fin (cardM bS adm).succ)) Finset.univ a ∧
          HSub.hSub (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) a.1 : R)
              ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) a.2 : R) =
            x) →
    ∃ (i : Fin (cardM bS adm).succ) (j : Fin (cardM bS adm).succ),
      i ≠ j ∧
        HSub.hSub (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) i : R)
            ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) j : R) =
          x
mpr :
  (∃ (i : Fin (cardM bS adm).succ) (j : Fin (cardM bS adm).succ),
      i ≠ j ∧
        HSub.hSub (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) i : R)
            ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) j : R) =
          x) →
    x ≠ 0 ∧
      ∃ (a : Fin (cardM bS adm).succ × Fin (cardM bS adm).succ),
        Membership.mem (γ := Finset (Fin (cardM bS adm).succ × Fin (cardM bS adm).succ)) Finset.univ a ∧
          HSub.hSub (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) a.1 : R)
              ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) a.2 : R) =
            x
⊢ (x ≠ 0 ∧
      ∃ (a : Fin (cardM bS adm).succ × Fin (cardM bS adm).succ),
        Membership.mem (γ := Finset (Fin (cardM bS adm).succ × Fin (cardM bS adm).succ)) Finset.univ a ∧
          HSub.hSub (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) a.1 : R)
              ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) a.2 : R) =
            x) ↔
    ∃ (i : Fin (cardM bS adm).succ) (j : Fin (cardM bS adm).succ),
      i ≠ j ∧
        HSub.hSub (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) i : R)
            ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) j : R) =
          x

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
i j : Fin (cardM bS adm).succ
left : Membership.mem (γ := Finset (Fin (cardM bS adm).succ × Fin (cardM bS adm).succ)) Finset.univ (i, j)
hx :
  HSub.hSub (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) (i, j).1 : R)
      ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) (i, j).2 : R) ≠
    0
⊢ ∃ (i_1 : Fin (cardM bS adm).succ) (j_1 : Fin (cardM bS adm).succ),
    i_1 ≠ j_1 ∧
      HSub.hSub (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) i_1 : R)
          ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) j_1 : R) =
        HSub.hSub (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) (i, j).1 : R)
          ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) (i, j).2 : R)

Tactic:
⟨i, j, ?_, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
i j : Fin (cardM bS adm).succ
left : Membership.mem (γ := Finset (Fin (cardM bS adm).succ × Fin (cardM bS adm).succ)) Finset.univ (i, j)
hx :
  HSub.hSub (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) (i, j).1 : R)
      ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) (i, j).2 : R) ≠
    0
mp : i ≠ j
⊢ ∃ (i_1 : Fin (cardM bS adm).succ) (j_1 : Fin (cardM bS adm).succ),
    i_1 ≠ j_1 ∧
      HSub.hSub (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) i_1 : R)
          ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) j_1 : R) =
        HSub.hSub (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) (i, j).1 : R)
          ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) (i, j).2 : R)

Tactic:
refine ⟨i, j, ?_, rfl⟩
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
i : Fin (cardM bS adm).succ
left : Membership.mem (γ := Finset (Fin (cardM bS adm).succ × Fin (cardM bS adm).succ)) Finset.univ (i, i)
hx :
  HSub.hSub (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) (i, i).1 : R)
      ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) (i, i).2 : R) ≠
    0
⊢ False

Tactic:
simp at hx
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
i j : Fin (cardM bS adm).succ
hij : i ≠ j
⊢ HSub.hSub (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) i : R)
        ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) j : R) ≠
      0 ∧
    ∃ (a : Fin (cardM bS adm).succ × Fin (cardM bS adm).succ),
      Membership.mem (γ := Finset (Fin (cardM bS adm).succ × Fin (cardM bS adm).succ)) Finset.univ a ∧
        HSub.hSub (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) a.1 : R)
            ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) a.2 : R) =
          HSub.hSub (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) i : R)
            ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) j : R)

Tactic:
⟨?_, ⟨i, j⟩, Finset.mem_univ _, rfl⟩

Premises used: Finset.mem_univ, Prod.mk, And.intro, Exists.intro, rfl
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
i j : Fin (cardM bS adm).succ
hij : i ≠ j
mpr :
  HSub.hSub (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) i : R)
      ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) j : R) ≠
    0
⊢ HSub.hSub (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) i : R)
        ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) j : R) ≠
      0 ∧
    ∃ (a : Fin (cardM bS adm).succ × Fin (cardM bS adm).succ),
      Membership.mem (γ := Finset (Fin (cardM bS adm).succ × Fin (cardM bS adm).succ)) Finset.univ a ∧
        HSub.hSub (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) a.1 : R)
            ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) a.2 : R) =
          HSub.hSub (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) i : R)
            ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) j : R)

Tactic:
refine ⟨?_, ⟨i, j⟩, Finset.mem_univ _, rfl⟩
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
i j : Fin (cardM bS adm).succ
hij : i ≠ j
mpr :
  ¬Eq (α := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) i : R)
      ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) j : R)
⊢ HSub.hSub (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) i : R)
      ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) j : R) ≠
    0

Tactic:
rw [Ne, sub_eq_zero]

Premises used: sub_eq_zero, Ne
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
i j : Fin (cardM bS adm).succ
hij : i ≠ j
⊢ ¬Eq (α := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) i : R)
      ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) j : R)

Tactic:
fun h => hij ((distinctElems bS adm).injective h)

Premises used: ClassGroup.distinctElems, Function.Embedding.injective, Not
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
i j : Fin (cardM bS adm).succ
hij : i ≠ j
⊢ ¬Eq (α := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) i : R)
      ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) j : R)

Tactic:
exact fun h => hij ((distinctElems bS adm).injective h)

Premises used: ClassGroup.distinctElems, Function.Embedding.injective
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
a : S
b : R
hb : b ≠ 0
⊢ 0 < Fintype.card ι

Tactic:
have dim_pos := Fintype.card_pos_iff.mpr bS.index_nonempty
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
⊢ let ε := HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ));
  ε = HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))

Tactic:
set ε : ℝ := normBound abv bS ^ (-1 / Fintype.card ι : ℝ) with ε_eq

Premises used: Fintype.card, HDiv.hDiv, Nat.cast, ClassGroup.normBound, OfNat.ofNat, Neg.neg
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
ε_eq : ε = HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
⊢ 0 < ε

Tactic:
have hε : 0 < ε := Real.rpow_pos_of_pos (Int.cast_pos.mpr (normBound_pos abv bS)) _
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
ε_eq : ε = HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
hε : 0 < ε
⊢ 0 < normBound abv bS

Tactic:
have := normBound_pos abv bS
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
ε_eq : ε = HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
hε : 0 < ε
this : 0 < normBound abv bS
⊢ LE.le (α := ℤ) (0 : ℤ) ((abv : (a : R) → ℤ) b : ℤ)

Tactic:
have := abv.nonneg b
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
ε_eq : ε = HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
hε : 0 < ε
this_1 : 0 < normBound abv bS
this : LE.le (α := ℤ) (0 : ℤ) ((abv : (a : R) → ℤ) b : ℤ)
rw : Ne (α := ℝ) (↑(normBound abv bS) : ℝ) 0
h : Ne (α := ℝ) (↑(Fintype.card ι) : ℝ) 0
hx : LE.le (α := ℝ) 0 (↑(normBound abv bS) : ℝ)
hx₁ : LE.le (α := ℝ) 0 (↑((abv : (a : R) → ℤ) b) : ℝ)
hy : 0 ≤ HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
⊢ (↑(normBound abv bS) : ℝ) *
      HPow.hPow (β := ℝ) (HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε) (↑(Fintype.card ι) : ℝ) ≤
    HPow.hPow (α := ℝ) (β := ℝ) (↑((abv : (a : R) → ℤ) b) : ℝ) (↑(Fintype.card ι) : ℝ)

Tactic:
rw [ε_eq, Algebra.smul_def, eq_intCast, mul_rpow, ← rpow_mul, div_mul_cancel₀, rpow_neg_one,
      mul_left_comm, mul_inv_cancel₀, mul_one, rpow_natCast]

Premises used: div_mul_cancel₀, Real.rpow_neg_one, mul_inv_cancel₀, Real.mul_rpow, eq_intCast, mul_left_comm, Algebra.smul_def, mul_one, Real.rpow_mul, Real.rpow_natCast
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
ε_eq : ε = HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
hε : 0 < ε
this_1 : 0 < normBound abv bS
this : LE.le (α := ℤ) (0 : ℤ) ((abv : (a : R) → ℤ) b : ℤ)
norm_cast : ¬normBound abv bS = 0
⊢ Ne (α := ℝ) (↑(normBound abv bS) : ℝ) 0

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
ε_eq : ε = HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
hε : 0 < ε
this_1 : 0 < normBound abv bS
this : LE.le (α := ℤ) (0 : ℤ) ((abv : (a : R) → ℤ) b : ℤ)
⊢ ¬normBound abv bS = 0

Tactic:
lia