awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ (t : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)),
      ∀ (i₀ i₁ : Fin n),
        t i₀ = t i₁ ↔
          (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
            HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
A : Fin (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i % b - A j % b)) : ℝ) < ε →
      (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A j % b - A k % b)) : ℝ) < ε →
        (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i % b - A k % b)) : ℝ) < ε
t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)
ht' :
  ∀ (i₀ i₁ : Fin n),
    t' i₀ = t' i₁ ↔
      (↑((cardPowDegree : (a : Fq[X]) → ℤ)
              (Fin.tail (α := fun (i : Fin (n + 1)) ↦ Fq[X]) A i₁ % b -
                Fin.tail (α := fun (i : Fin (n + 1)) ↦ Fq[X]) A i₀ % b)) :
          ℝ) <
        HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
j_1 : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)
hj_1 :
  ∀ (i : Fin n),
    t' i = j_1 →
      (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A i.succ % b)) : ℝ) <
        HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)
hj :
  ∀ (i : Fin n),
    t' i = j →
      (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A i.succ % b)) : ℝ) <
        HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
i : Fin n
hi : t' i = j
i' : Fin n
hi' :
  (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A i'.succ % b)) : ℝ) <
    HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
⊢ (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i.succ % b - A 0 % b)) : ℝ) <
    HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
have rw : (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A i.succ % b)) : ℝ) <
  HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
Tactic: rw [AbsoluteValue.map_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ (t : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)),
      ∀ (i₀ i₁ : Fin n),
        t i₀ = t i₁ ↔
          (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
            HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
A : Fin (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i % b - A j % b)) : ℝ) < ε →
      (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A j % b - A k % b)) : ℝ) < ε →
        (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i % b - A k % b)) : ℝ) < ε
t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)
ht' :
  ∀ (i₀ i₁ : Fin n),
    t' i₀ = t' i₁ ↔
      (↑((cardPowDegree : (a : Fq[X]) → ℤ)
              (Fin.tail (α := fun (i : Fin (n + 1)) ↦ Fq[X]) A i₁ % b -
                Fin.tail (α := fun (i : Fin (n + 1)) ↦ Fq[X]) A i₀ % b)) :
          ℝ) <
        HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)
hj :
  ∀ (i : Fin n),
    t' i = j →
      (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A i.succ % b)) : ℝ) <
        HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
exists_nonempty_j :
  ¬∃ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)),
      (∃ (i : Fin n), t' i = j) ∧
        ∀ (i : Fin n),
          t' i = j →
            (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A i.succ % b)) : ℝ) <
              HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
⊢ ∃ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)),
    ∀ (i : Fin n),
      t' i = j ↔
        (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A i.succ % b)) : ℝ) <
          HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
have neg : ∀ (i : Fin n)
  (hi :
    (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A i.succ % b)) : ℝ) <
      HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε),
  t' i = j
Tactic: refine ⟨j, fun i => ⟨hj i, fun hi => ?_⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (hypothesis)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ (t : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)),
      ∀ (i₀ i₁ : Fin n),
        t i₀ = t i₁ ↔
          (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
            HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
A : Fin (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i % b - A j % b)) : ℝ) < ε →
      (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A j % b - A k % b)) : ℝ) < ε →
        (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i % b - A k % b)) : ℝ) < ε
t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)
ht' :
  ∀ (i₀ i₁ : Fin n),
    t' i₀ = t' i₁ ↔
      (↑((cardPowDegree : (a : Fq[X]) → ℤ)
              (Fin.tail (α := fun (i : Fin (n + 1)) ↦ Fq[X]) A i₁ % b -
                Fin.tail (α := fun (i : Fin (n + 1)) ↦ Fq[X]) A i₀ % b)) :
          ℝ) <
        HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)
hj :
  ∀ (i : Fin n),
    t' i = j →
      (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A i.succ % b)) : ℝ) <
        HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
exists_nonempty_j :
  ¬∃ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)),
      (∃ (i : Fin n), t' i = j) ∧
        ∀ (i : Fin n),
          t' i = j →
            (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A i.succ % b)) : ℝ) <
              HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
i : Fin n
hi :
  (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A i.succ % b)) : ℝ) <
    HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
⊢ t' i = j
have this : False
Tactic: have := exists_nonempty_j ⟨t' i, ⟨i, rfl⟩, fun i' hi' => anti_archim' hi ((ht' _ _).mp hi')⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
n : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A : Fin n → Fq[X]
⊢ ∃ (t : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)),
    ∀ (i₀ i₁ : Fin n),
      t i₀ = t i₁ →
        (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
          HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
have obtain : ∀ (t : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊))
  (ht :
    ∀ (i₀ i₁ : Fin n),
      t i₀ = t i₁ ↔
        (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
          HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε),
  ∃ (t : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)),
    ∀ (i₀ i₁ : Fin n),
      t i₀ = t i₁ →
        (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
          HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
Tactic: obtain ⟨t, ht⟩ := exists_partition_polynomial_aux n hε hb A
-- 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
⊢ ∃ (i : ι) (j : ι) (k : ι),
    Ne.{u_1 + 1} (α := R) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) j k : R) (0 : R)
have by_contra! : ∀
  (h :
    ∀ (i j k : ι),
      Eq.{u_1 + 1} (α := R) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) j k : R)
        (0 : R)),
  False
Tactic: by_contra! h
-- 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
h :
  ∀ (i j k : ι),
    Eq.{u_1 + 1} (α := R) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) j k : R) (0 : R)
⊢ False
have obtain : ∀ (i : ι), False
Tactic: obtain ⟨i⟩ := bS.index_nonempty
-- 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
h :
  ∀ (i j k : ι),
    Eq.{u_1 + 1} (α := R) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) j k : R) (0 : R)
i : ι
⊢ False
have apply : Eq.{u_2 + 1} (α := S) ((bS : (a : ι) → S) i : S) (0 : S)
Tactic: apply bS.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 ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
h :
  ∀ (i j k : ι),
    Eq.{u_1 + 1} (α := R) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) j k : R) (0 : R)
i : ι
⊢ Eq.{u_2 + 1} (α := S) ((bS : (a : ι) → S) i : S) (0 : S)
have a : Eq (α := Matrix ι ι R) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) : Matrix ι ι R)
  (0 : Matrix ι ι R)
Tactic: apply
      (injective_iff_map_eq_zero (Algebra.leftMulMatrix bS)).mp (Algebra.leftMulMatrix_injective bS)
-- 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
h :
  ∀ (i j k : ι),
    Eq.{u_1 + 1} (α := R) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) j k : R) (0 : R)
i : ι
⊢ Eq (α := Matrix ι ι R) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) : Matrix ι ι R)
    (0 : Matrix ι ι R)
have a : ∀ (j k : ι),
  Eq.{u_1 + 1} (α := R) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) j k : R) (0 j k : R)
Tactic: ext j k
-- 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
⊢ 0 < normBound abv bS
have obtain : ∀ (i j k : ι)
  (hijk :
    Ne.{u_1 + 1} (α := R) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) j k : R) (0 : R)),
  0 < normBound abv bS
Tactic: obtain ⟨i, j, k, hijk⟩ : ∃ i j k, Algebra.leftMulMatrix bS (bS i) j k ≠ 0 := by
    by_contra! h
    obtain ⟨i⟩ := bS.index_nonempty
    apply bS.ne_zero i
    apply
      (injective_iff_map_eq_zero (Algebra.leftMulMatrix bS)).mp (Algebra.leftMulMatrix_injective bS)
    ext j k
    simp [h]
-- 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
i j k : ι
hijk :
  Ne.{u_1 + 1} (α := R) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) j k : R) (0 : R)
⊢ 0 <
    (↑(Fintype.card ι).factorial : ℤ) *
      ((↑(Fintype.card ι) : ℤ) *
          Finset.max'
            (Finset.image
              (fun (ijk : ι × ι × ι) ↦
                (abv : (a : R) → ℤ)
                  ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
              Finset.univ)
            ⋯) ^
        Fintype.card ι
have apply : 0 <
  ((↑(Fintype.card ι) : ℤ) *
      Finset.max'
        (Finset.image
          (fun (ijk : ι × ι × ι) ↦
            (abv : (a : R) → ℤ)
              ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
          Finset.univ)
        sorry) ^
    Fintype.card ι
Tactic: apply mul_pos (Int.natCast_pos.mpr (Nat.factorial_pos _))
-- 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
i j k : ι
hijk :
  Ne.{u_1 + 1} (α := R) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) j k : R) (0 : R)
⊢ 0 <
    ((↑(Fintype.card ι) : ℤ) *
        Finset.max'
          (Finset.image
            (fun (ijk : ι × ι × ι) ↦
              (abv : (a : R) → ℤ)
                ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
            Finset.univ)
          ⋯) ^
      Fintype.card ι
have refine : 0 <
  Finset.max'
    (Finset.image
      (fun (ijk : ι × ι × ι) ↦
        (abv : (a : R) → ℤ)
          ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
      Finset.univ)
    sorry
Tactic: refine pow_pos (mul_pos (Int.natCast_pos.mpr (Fintype.card_pos_iff.mpr ⟨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 ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
i j k : ι
hijk :
  Ne.{u_1 + 1} (α := R) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) j k : R) (0 : R)
⊢ 0 <
    Finset.max'
      (Finset.image
        (fun (ijk : ι × ι × ι) ↦
          (abv : (a : R) → ℤ)
            ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
        Finset.univ)
      ⋯
have refine : Membership.mem (α := ℤ) (γ := Finset ℤ)
  (Finset.image
    (fun (ijk : ι × ι × ι) ↦
      (abv : (a : R) → ℤ)
        ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
    Finset.univ)
  ((abv : (a : R) → ℤ) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) j k : R) : ℤ)
Tactic: refine lt_of_lt_of_le (abv.pos hijk) (Finset.le_max' _ _ ?_)
-- 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
a : S
y : ℤ
hy : ∀ (k : ι), (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y
| ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) a : R) : ℤ)
have rw : ((abv : (a : R) → ℤ)
    ((Algebra.norm R : (a : S) → R)
        (∑ i : ι,
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
            ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) i : R) ((bS : (a : ι) → S) i : S)) :
      R) :
  ℤ)
Tactic: rw [← bS.sum_repr a]
-- 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
a : S
y : ℤ
hy : ∀ (k : ι), (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y
⊢ (abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) a : R) ≤ normBound abv bS * y ^ Fintype.card ι
have conv_lhs : (abv : (a : R) → ℤ)
    ((Algebra.norm R : (a : S) → R)
        (∑ i : ι,
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
            ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) i : R) ((bS : (a : ι) → S) i : S)) :
      R) ≤
  normBound abv bS * y ^ Fintype.card ι
Tactic: conv_lhs => rw [← bS.sum_repr a]
-- 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
a : S
y : ℤ
hy : ∀ (k : ι), (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y
⊢ (abv : (a : R) → ℤ)
      ((Algebra.norm R : (a : S) → R)
          (∑ i : ι,
            HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
              ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) i : R) ((bS : (a : ι) → S) i : S)) :
        R) ≤
    normBound abv bS * y ^ Fintype.card ι
have rw : (abv : (a : R) → ℤ)
    (Matrix.det.{u_1, u_5} (n := ι)
      ((LinearMap.toMatrix bS bS : (a : S →ₗ[R] S) → Matrix ι ι R)
        ((Algebra.lmul R S : (a : S) → End R S)
          (∑ i : ι,
            HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
              ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) i : R) ((bS : (a : ι) → S) i : S))))) ≤
  normBound abv bS * y ^ Fintype.card ι
Tactic: rw [Algebra.norm_apply, ← LinearMap.det_toMatrix bS]
-- 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
a : S
y : ℤ
hy : ∀ (k : ι), (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y
⊢ (abv : (a : R) → ℤ)
      (Matrix.det.{u_1, u_5} (n := ι)
        ((LinearMap.toMatrix bS bS : (a : S →ₗ[R] S) → Matrix ι ι R)
          ((Algebra.lmul R S : (a : S) → End R S)
            (∑ i : ι,
              HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
                ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) i : R) ((bS : (a : ι) → S) i : S))))) ≤
    normBound abv bS * y ^ Fintype.card ι
have simp : (abv : (a : R) → ℤ)
    (Matrix.det.{u_1, u_5} (n := ι)
      (∑ x : ι,
        HSMul.hSMul (α := R) (β := Matrix ι ι R) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) x : R)
          ((LinearMap.toMatrix bS bS : (a : S →ₗ[R] S) → Matrix ι ι R)
              ((Algebra.lmul R S : (a : S) → End R S) ((bS : (a : ι) → S) x : S)) :
            Matrix ι ι R))) ≤
  (Fintype.card ι).factorial •
    (Fintype.card ι •
        (Finset.max'
            (Finset.image
              (fun (ijk : ι × ι × ι) ↦
                (abv : (a : R) → ℤ)
                  ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
              Finset.univ)
            sorry *
          y)) ^
      Fintype.card ι
Tactic: simp only [map_sum, map_smul, map_sum, map_smul,
    normBound, smul_mul_assoc, ← mul_pow]
-- 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
a : S
y : ℤ
hy : ∀ (k : ι), (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y
⊢ (abv : (a : R) → ℤ)
      (Matrix.det.{u_1, u_5} (n := ι)
        (∑ x : ι,
          HSMul.hSMul (α := R) (β := Matrix ι ι R) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) x : R)
            ((LinearMap.toMatrix bS bS : (a : S →ₗ[R] S) → Matrix ι ι R)
                ((Algebra.lmul R S : (a : S) → End R S) ((bS : (a : ι) → S) x : S)) :
              Matrix ι ι R))) ≤
    (Fintype.card ι).factorial •
      (Fintype.card ι •
          (Finset.max'
              (Finset.image
                (fun (ijk : ι × ι × ι) ↦
                  (abv : (a : R) → ℤ)
                    ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 :
                      R))
                Finset.univ)
              ⋯ *
            y)) ^
        Fintype.card ι
have h : Fintype.card ι •
    (Finset.max'
        (Finset.image
          (fun (ijk : ι × ι × ι) ↦
            (abv : (a : R) → ℤ)
              ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
          Finset.univ)
        sorry *
      y) =
  Finset.card.{u_5} (α := ι) Finset.univ • y *
    Finset.max'
      (Finset.image
        (fun (ijk : ι × ι × ι) ↦
          (abv : (a : R) → ℤ)
            ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
        Finset.univ)
      sorry
Tactic: convert! Matrix.det_sum_smul_le Finset.univ _ hy using 3
-- 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
a : S
y : ℤ
hy : ∀ (k : ι), (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y
h :
  Fintype.card ι •
      (Finset.max'
          (Finset.image
            (fun (ijk : ι × ι × ι) ↦
              (abv : (a : R) → ℤ)
                ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
            Finset.univ)
          ⋯ *
        y) =
    Finset.card.{u_5} (α := ι) Finset.univ • y *
      Finset.max'
        (Finset.image
          (fun (ijk : ι × ι × ι) ↦
            (abv : (a : R) → ℤ)
              ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
          Finset.univ)
        ⋯
convert_5 : ℤ
⊢ (abv : (a : R) → ℤ)
      (Matrix.det.{u_1, u_5} (n := ι)
        (∑ x : ι,
          HSMul.hSMul (α := R) (β := Matrix ι ι R) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) x : R)
            ((LinearMap.toMatrix bS bS : (a : S →ₗ[R] S) → Matrix ι ι R)
                ((Algebra.lmul R S : (a : S) → End R S) ((bS : (a : ι) → S) x : S)) :
              Matrix ι ι R))) ≤
    (Fintype.card ι).factorial •
      (Fintype.card ι •
          (Finset.max'
              (Finset.image
                (fun (ijk : ι × ι × ι) ↦
                  (abv : (a : R) → ℤ)
                    ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 :
                      R))
                Finset.univ)
              ⋯ *
            y)) ^
        Fintype.card ι
have convert_6 : ∀ (k i j : ι),
  (abv : (a : R) → ℤ)
      ((LinearMap.toMatrix bS bS : (a : S →ₗ[R] S) → Matrix ι ι R)
          ((Algebra.lmul R S : (a : S) → End R S) ((bS : (a : ι) → S) k : S)) i j :
        R) ≤
    Finset.max'
      (Finset.image
        (fun (ijk : ι × ι × ι) ↦
          (abv : (a : R) → ℤ)
            ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
        Finset.univ)
      sorry
Tactic: convert! Matrix.det_sum_smul_le Finset.univ _ hy using 3