awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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
T : Type u_6
inst_6 : Ring T
inst_7 : LinearOrder T
inst_8 : IsStrictOrderedRing T
a : S
y : T
hy : ∀ (k : ι), (↑((abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R)) : T) < y
i : ι
him :
  Finset.Nonempty (α := ℤ)
    (Finset.image (fun (k : ι) ↦ (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R))
      Finset.univ)
y' : ℤ :=
  Finset.max'
    (Finset.image (fun (k : ι) ↦ (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R))
      Finset.univ)
    him
y'_def :
  y' =
    Finset.max'
      (Finset.image
        (fun (k : ι) ↦ (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R))
        Finset.univ)
      him
hy' : ∀ (k : ι), (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y'
this : (↑y' : T) < y
y'_nonneg : 0 ≤ y'
⊢ (↑(normBound abv bS) : T) * HPow.hPow (α := T) (↑y' : T) (Fintype.card ι) <
    (↑(normBound abv bS) : T) * y ^ Fintype.card ι
have h₂ : HPow.hPow (α := T) (↑y' : T) (Fintype.card ι) < y ^ Fintype.card ι
Tactic: apply mul_lt_mul' le_rfl
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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
T : Type u_6
inst_6 : Ring T
inst_7 : LinearOrder T
inst_8 : IsStrictOrderedRing T
a : S
y : T
hy : ∀ (k : ι), (↑((abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R)) : T) < y
i : ι
him :
  Finset.Nonempty (α := ℤ)
    (Finset.image (fun (k : ι) ↦ (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R))
      Finset.univ)
y' : ℤ :=
  Finset.max'
    (Finset.image (fun (k : ι) ↦ (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R))
      Finset.univ)
    him
y'_def :
  y' =
    Finset.max'
      (Finset.image
        (fun (k : ι) ↦ (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R))
        Finset.univ)
      him
hy' : ∀ (k : ι), (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y'
this : (↑y' : T) < y
y'_nonneg : 0 ≤ y'
h₂ : HPow.hPow (α := T) (↑y' : T) (Fintype.card ι) < y ^ Fintype.card ι
⊢ (↑(normBound abv bS) : T) * HPow.hPow (α := T) (↑y' : T) (Fintype.card ι) <
    (↑(normBound abv bS) : T) * y ^ Fintype.card ι
have c0 : 0 ≤ HPow.hPow (α := T) (↑y' : T) (Fintype.card ι)
Tactic: apply mul_lt_mul' le_rfl
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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
T : Type u_6
inst_6 : Ring T
inst_7 : LinearOrder T
inst_8 : IsStrictOrderedRing T
a : S
y : T
hy : ∀ (k : ι), (↑((abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R)) : T) < y
i : ι
him :
  Finset.Nonempty (α := ℤ)
    (Finset.image (fun (k : ι) ↦ (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R))
      Finset.univ)
y' : ℤ :=
  Finset.max'
    (Finset.image (fun (k : ι) ↦ (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R))
      Finset.univ)
    him
y'_def :
  y' =
    Finset.max'
      (Finset.image
        (fun (k : ι) ↦ (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R))
        Finset.univ)
      him
hy' : ∀ (k : ι), (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y'
this : (↑y' : T) < y
y'_nonneg : 0 ≤ y'
h₂ : HPow.hPow (α := T) (↑y' : T) (Fintype.card ι) < y ^ Fintype.card ι
c0 : 0 ≤ HPow.hPow (α := T) (↑y' : T) (Fintype.card ι)
⊢ (↑(normBound abv bS) : T) * HPow.hPow (α := T) (↑y' : T) (Fintype.card ι) <
    (↑(normBound abv bS) : T) * y ^ Fintype.card ι
have b0 : LT.lt.{u_6} (α := T) 0 (↑(normBound abv bS) : T)
Tactic: apply mul_lt_mul' le_rfl
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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 : ℤ),
    ∀ (z : ℤ),
      (fun (a : ℤ) ↦ ∃ b ∈ (↑I : Ideal S), b ≠ 0 ∧ (abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) = a) z →
        b ≤ z
have h : ∀ (z : ℤ),
  (fun (a : ℤ) ↦ ∃ b ∈ (↑I : Ideal S), b ≠ 0 ∧ (abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) = a) z → 0 ≤ z
Tactic: use 0
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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)⁰
⊢ ∃ (z : ℤ),
    (fun (a : ℤ) ↦ ∃ b ∈ (↑I : Ideal S), b ≠ 0 ∧ (abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) = a) z
have obtain : ∀ (b : S) (b_mem : b ∈ (↑I : Ideal S)) (b_ne_zero : b ≠ 0),
  ∃ (z : ℤ),
    (fun (a : ℤ) ↦ ∃ b ∈ (↑I : Ideal S), b ≠ 0 ∧ (abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) = a) z
Tactic: obtain ⟨b, b_mem, b_ne_zero⟩ := (I : Ideal S).ne_bot_iff.mp (nonZeroDivisors.coe_ne_zero I)
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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 ∈ (↑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
have 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
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⟩⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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
have 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
Tactic: refine ⟨b, b_mem, b_ne_zero, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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) : ℤ)
⊢ c = 0
have 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) : ℤ)
Tactic: contrapose! lt with c_ne_zero
Cleared hypotheses: lt
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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
⊢ 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
have 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
Tactic: simp only [finsetApprox, Finset.mem_erase, Finset.mem_image]
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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
⊢ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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
⊢ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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)
have mp : i ≠ j
Tactic: refine ⟨i, j, ?_, rfl⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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)
have 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
Tactic: refine ⟨?_, ⟨i, j⟩, Finset.mem_univ _, rfl⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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
have 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)
Tactic: rw [Ne, sub_eq_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (hypothesis)
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
⊢ ∃ (q : S),
    ∃ r ∈ finsetApprox bS adm,
      LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a - b • q) : R) : ℤ)
        ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b : S) : R) : ℤ)
have dim_pos : 0 < Fintype.card ι
Tactic: have dim_pos := Fintype.card_pos_iff.mpr bS.index_nonempty
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (hypothesis)
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 ι
⊢ ∃ (q : S),
    ∃ r ∈ finsetApprox bS adm,
      LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a - b • q) : R) : ℤ)
        ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b : S) : R) : ℤ)
have ε_eq : 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
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (hypothesis)
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 ι) : ℝ))
⊢ ∃ (q : S),
    ∃ r ∈ finsetApprox bS adm,
      LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a - b • q) : R) : ℤ)
        ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b : S) : R) : ℤ)
have hε : 0 < ε
Tactic: have hε : 0 < ε := Real.rpow_pos_of_pos (Int.cast_pos.mpr (normBound_pos abv bS)) _
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (hypothesis)
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 < ε
⊢ (↑(normBound abv bS) : ℝ) *
      HPow.hPow (β := ℝ) (HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε) (↑(Fintype.card ι) : ℝ) ≤
    HPow.hPow (α := ℝ) (β := ℝ) (↑((abv : (a : R) → ℤ) b) : ℝ) (↑(Fintype.card ι) : ℝ)
have this : 0 < normBound abv bS
Tactic: have := normBound_pos abv bS
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (hypothesis)
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
⊢ (↑(normBound abv bS) : ℝ) *
      HPow.hPow (β := ℝ) (HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε) (↑(Fintype.card ι) : ℝ) ≤
    HPow.hPow (α := ℝ) (β := ℝ) (↑((abv : (a : R) → ℤ) b) : ℝ) (↑(Fintype.card ι) : ℝ)
have this₁ : LE.le (α := ℤ) (0 : ℤ) ((abv : (a : R) → ℤ) b : ℤ)
Tactic: have := abv.nonneg b
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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) : ℝ) *
      HPow.hPow (β := ℝ) (HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε) (↑(Fintype.card ι) : ℝ) ≤
    HPow.hPow (α := ℝ) (β := ℝ) (↑((abv : (a : R) → ℤ) b) : ℝ) (↑(Fintype.card ι) : ℝ)
have rw : Ne (α := ℝ) (↑(normBound abv bS) : ℝ) 0
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]