awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
A : Type u_2
inst : Field A
inst_1 : CharZero A
p : IntermediateField ℚ A → Prop
S : Set { F : IntermediateField ℚ A // p F }
T : Set A
hT : T.Finite
h : ∀ F ∈ S, ∃ x ∈ T, (↑F : IntermediateField ℚ A) = ℚ⟮x⟯
⊢ Finite.{u_2 + 1} (↑T : Type u_2)

Tactic:
rw [← Set.finite_coe_iff] at hT

Premises used: Set.finite_coe_iff
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
A : Type u_2
inst : Field A
inst_1 : CharZero A
p : IntermediateField ℚ A → Prop
S : Set { F : IntermediateField ℚ A // p F }
T : Set A
hT : T.Finite
h : ∀ F ∈ S, ∃ x ∈ T, (↑F : IntermediateField ℚ A) = ℚ⟮x⟯
hT₁ : Finite.{u_2 + 1} (↑T : Type u_2)
⊢ ∀ F ∈ S, ∃ x ∈ T, (↑F : IntermediateField ℚ A) = ℚ⟮x⟯

Tactic:
rw [← Set.finite_coe_iff] at hT

Premises used: Set.finite_coe_iff
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
A : Type u_2
inst : Field A
inst_1 : CharZero A
p : IntermediateField ℚ A → Prop
S : Set { F : IntermediateField ℚ A // p F }
T : Set A
hT : Finite.{u_2 + 1} (↑T : Type u_2)
h : ∀ F ∈ S, ∃ x ∈ T, (↑F : IntermediateField ℚ A) = ℚ⟮x⟯
⊢ S.Finite

Tactic:
Set.finite_coe_iff.mp <| Finite.of_injective
    (fun ⟨F, hF⟩ ↦ (⟨(h F hF).choose, (h F hF).choose_spec.1⟩ : T)) (fun _ _ h_eq ↦ ?_)

Premises used: Set.finite_coe_iff, Iff.mp, Finite.of_injective
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
A : Type u_2
inst : Field A
inst_1 : CharZero A
p : IntermediateField ℚ A → Prop
S : Set { F : IntermediateField ℚ A // p F }
T : Set A
hT : Finite.{u_2 + 1} (↑T : Type u_2)
h : ∀ F ∈ S, ∃ x ∈ T, (↑F : IntermediateField ℚ A) = ℚ⟮x⟯
refine :
  ∀ (x x_1 : (↑S : Type u_2))
    (h_eq :
      Eq.{u_2 + 1} (α := { x : A // x ∈ T })
        ((fun (x : (↑S : Type u_2)) ↦
            (match (motive := (↑S : Type u_2) → { x : A // x ∈ T }) x with
              | ⟨F, hF⟩ =>
                Subtype.mk (p := fun (x : A) ↦ x ∈ T)
                  (⋯.choose (p := fun (x : A) ↦ x ∈ T ∧ (↑F : IntermediateField ℚ A) = ℚ⟮x⟯)) ⋯ :
              { x : A // x ∈ T }))
          x)
        ((fun (x : (↑S : Type u_2)) ↦
            (match (motive := (↑S : Type u_2) → { x : A // x ∈ T }) x with
              | ⟨F, hF⟩ =>
                Subtype.mk (p := fun (x : A) ↦ x ∈ T)
                  (⋯.choose (p := fun (x : A) ↦ x ∈ T ∧ (↑F : IntermediateField ℚ A) = ℚ⟮x⟯)) ⋯ :
              { x : A // x ∈ T }))
          x_1)),
    x = x_1
⊢ S.Finite

Tactic:
refine Set.finite_coe_iff.mp <| Finite.of_injective
    (fun ⟨F, hF⟩ ↦ (⟨(h F hF).choose, (h F hF).choose_spec.1⟩ : T)) (fun _ _ h_eq ↦ ?_)

Premises used: Set.finite_coe_iff, Iff.mp, Finite.of_injective
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
A : Type u_2
inst : Field A
inst_1 : CharZero A
p : IntermediateField ℚ A → Prop
S : Set { F : IntermediateField ℚ A // p F }
T : Set A
hT : Finite.{u_2 + 1} (↑T : Type u_2)
h : ∀ F ∈ S, ∃ x ∈ T, (↑F : IntermediateField ℚ A) = ℚ⟮x⟯
x x_1 : (↑S : Type u_2)
h_eq :
  Eq.{u_2 + 1} (α := { x : A // x ∈ T })
    ((fun (x : (↑S : Type u_2)) ↦
        (match (motive := (↑S : Type u_2) → { x : A // x ∈ T }) x with
          | ⟨F, hF⟩ =>
            Subtype.mk (p := fun (x : A) ↦ x ∈ T)
              (⋯.choose (p := fun (x : A) ↦ x ∈ T ∧ (↑F : IntermediateField ℚ A) = ℚ⟮x⟯)) ⋯ :
          { x : A // x ∈ T }))
      x)
    ((fun (x : (↑S : Type u_2)) ↦
        (match (motive := (↑S : Type u_2) → { x : A // x ∈ T }) x with
          | ⟨F, hF⟩ =>
            Subtype.mk (p := fun (x : A) ↦ x ∈ T)
              (⋯.choose (p := fun (x : A) ↦ x ∈ T ∧ (↑F : IntermediateField ℚ A) = ℚ⟮x⟯)) ⋯ :
          { x : A // x ∈ T }))
      x_1)
rw :
  (↑(↑x : { F : IntermediateField ℚ A // p F }) : IntermediateField ℚ A) =
    (↑(↑x_1 : { F : IntermediateField ℚ A // p F }) : IntermediateField ℚ A)
⊢ x = x_1

Tactic:
rw [Subtype.ext_iff, Subtype.ext_iff]

Premises used: Subtype.ext_iff
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
A : Type u_2
inst : Field A
inst_1 : CharZero A
p : IntermediateField ℚ A → Prop
S : Set { F : IntermediateField ℚ A // p F }
T : Set A
hT : Finite.{u_2 + 1} (↑T : Type u_2)
h : ∀ F ∈ S, ∃ x ∈ T, (↑F : IntermediateField ℚ A) = ℚ⟮x⟯
x x_1 : (↑S : Type u_2)
h_eq :
  Eq.{u_2 + 1} (α := { x : A // x ∈ T })
    ((fun (x : (↑S : Type u_2)) ↦
        (match (motive := (↑S : Type u_2) → { x : A // x ∈ T }) x with
          | ⟨F, hF⟩ =>
            Subtype.mk (p := fun (x : A) ↦ x ∈ T)
              (⋯.choose (p := fun (x : A) ↦ x ∈ T ∧ (↑F : IntermediateField ℚ A) = ℚ⟮x⟯)) ⋯ :
          { x : A // x ∈ T }))
      x)
    ((fun (x : (↑S : Type u_2)) ↦
        (match (motive := (↑S : Type u_2) → { x : A // x ∈ T }) x with
          | ⟨F, hF⟩ =>
            Subtype.mk (p := fun (x : A) ↦ x ∈ T)
              (⋯.choose (p := fun (x : A) ↦ x ∈ T ∧ (↑F : IntermediateField ℚ A) = ℚ⟮x⟯)) ⋯ :
          { x : A // x ∈ T }))
      x_1)
⊢ Eq.{u_2 + 1} (α := IntermediateField ℚ A)
    ((fun (x : A) ↦ (ℚ⟮x⟯ : IntermediateField ℚ A))
      (⋯.choose (p := fun (x_2 : A) ↦
        x_2 ∈ T ∧ (↑(↑x : { F : IntermediateField ℚ A // p F }) : IntermediateField ℚ A) = ℚ⟮x_2⟯)))
    ((fun (x : A) ↦ (ℚ⟮x⟯ : IntermediateField ℚ A))
      (⋯.choose (p := fun (x : A) ↦
        x ∈ T ∧ (↑(↑x_1 : { F : IntermediateField ℚ A // p F }) : IntermediateField ℚ A) = ℚ⟮x⟯)))

Tactic:
congr_arg (ℚ⟮·⟯) (Subtype.mk_eq_mk.mp h_eq)

Premises used: Rat, congr_arg, IntermediateField.adjoin, Subtype.mk_eq_mk, Iff.mp, Singleton.singleton
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
A : Type u_2
inst : Field A
inst_1 : CharZero A
p : IntermediateField ℚ A → Prop
S : Set { F : IntermediateField ℚ A // p F }
T : Set A
hT : Finite.{u_2 + 1} (↑T : Type u_2)
h : ∀ F ∈ S, ∃ x ∈ T, (↑F : IntermediateField ℚ A) = ℚ⟮x⟯
x x_1 : (↑S : Type u_2)
h_eq :
  Eq.{u_2 + 1} (α := { x : A // x ∈ T })
    ((fun (x : (↑S : Type u_2)) ↦
        (match (motive := (↑S : Type u_2) → { x : A // x ∈ T }) x with
          | ⟨F, hF⟩ =>
            Subtype.mk (p := fun (x : A) ↦ x ∈ T)
              (⋯.choose (p := fun (x : A) ↦ x ∈ T ∧ (↑F : IntermediateField ℚ A) = ℚ⟮x⟯)) ⋯ :
          { x : A // x ∈ T }))
      x)
    ((fun (x : (↑S : Type u_2)) ↦
        (match (motive := (↑S : Type u_2) → { x : A // x ∈ T }) x with
          | ⟨F, hF⟩ =>
            Subtype.mk (p := fun (x : A) ↦ x ∈ T)
              (⋯.choose (p := fun (x : A) ↦ x ∈ T ∧ (↑F : IntermediateField ℚ A) = ℚ⟮x⟯)) ⋯ :
          { x : A // x ∈ T }))
      x_1)
h₁ :
  (↑(↑x : { F : IntermediateField ℚ A // p F }) : IntermediateField ℚ A) =
    ℚ⟮⋯.choose (p := fun (x_2 : A) ↦
        x_2 ∈ T ∧ (↑(↑x : { F : IntermediateField ℚ A // p F }) : IntermediateField ℚ A) = ℚ⟮x_2⟯)⟯
h₂ :
  (↑(↑x_1 : { F : IntermediateField ℚ A // p F }) : IntermediateField ℚ A) =
    ℚ⟮⋯.choose (p := fun (x : A) ↦
        x ∈ T ∧ (↑(↑x_1 : { F : IntermediateField ℚ A // p F }) : IntermediateField ℚ A) = ℚ⟮x⟯)⟯
⊢ (↑(↑x : { F : IntermediateField ℚ A // p F }) : IntermediateField ℚ A) =
    (↑(↑x_1 : { F : IntermediateField ℚ A // p F }) : IntermediateField ℚ A)

Tactic:
convert! congr_arg (ℚ⟮·⟯) (Subtype.mk_eq_mk.mp h_eq)

Premises used: Rat, congr_arg, IntermediateField.adjoin, Subtype.mk_eq_mk, Iff.mp, Singleton.singleton
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
A : Type u_2
inst : Field A
inst_1 : CharZero A
p : IntermediateField ℚ A → Prop
S : Set { F : IntermediateField ℚ A // p F }
T : Set A
hT : Finite.{u_2 + 1} (↑T : Type u_2)
h : ∀ F ∈ S, ∃ x ∈ T, (↑F : IntermediateField ℚ A) = ℚ⟮x⟯
x x_1 : (↑S : Type u_2)
h_eq :
  Eq.{u_2 + 1} (α := { x : A // x ∈ T })
    ((fun (x : (↑S : Type u_2)) ↦
        (match (motive := (↑S : Type u_2) → { x : A // x ∈ T }) x with
          | ⟨F, hF⟩ =>
            Subtype.mk (p := fun (x : A) ↦ x ∈ T)
              (⋯.choose (p := fun (x : A) ↦ x ∈ T ∧ (↑F : IntermediateField ℚ A) = ℚ⟮x⟯)) ⋯ :
          { x : A // x ∈ T }))
      x)
    ((fun (x : (↑S : Type u_2)) ↦
        (match (motive := (↑S : Type u_2) → { x : A // x ∈ T }) x with
          | ⟨F, hF⟩ =>
            Subtype.mk (p := fun (x : A) ↦ x ∈ T)
              (⋯.choose (p := fun (x : A) ↦ x ∈ T ∧ (↑F : IntermediateField ℚ A) = ℚ⟮x⟯)) ⋯ :
          { x : A // x ∈ T }))
      x_1)
⊢ (↑(↑x : { F : IntermediateField ℚ A // p F }) : IntermediateField ℚ A) =
    ℚ⟮⋯.choose (p := fun (x_2 : A) ↦
        x_2 ∈ T ∧ (↑(↑x : { F : IntermediateField ℚ A // p F }) : IntermediateField ℚ A) = ℚ⟮x_2⟯)⟯

Tactic:
(h _ (Subtype.mem _)).choose_spec.2

Premises used: Exists.choose_spec, And.right, Subtype.mem
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
A : Type u_2
inst : Field A
inst_1 : CharZero A
p : IntermediateField ℚ A → Prop
S : Set { F : IntermediateField ℚ A // p F }
T : Set A
hT : Finite.{u_2 + 1} (↑T : Type u_2)
h : ∀ F ∈ S, ∃ x ∈ T, (↑F : IntermediateField ℚ A) = ℚ⟮x⟯
x x_1 : (↑S : Type u_2)
h_eq :
  Eq.{u_2 + 1} (α := { x : A // x ∈ T })
    ((fun (x : (↑S : Type u_2)) ↦
        (match (motive := (↑S : Type u_2) → { x : A // x ∈ T }) x with
          | ⟨F, hF⟩ =>
            Subtype.mk (p := fun (x : A) ↦ x ∈ T)
              (⋯.choose (p := fun (x : A) ↦ x ∈ T ∧ (↑F : IntermediateField ℚ A) = ℚ⟮x⟯)) ⋯ :
          { x : A // x ∈ T }))
      x)
    ((fun (x : (↑S : Type u_2)) ↦
        (match (motive := (↑S : Type u_2) → { x : A // x ∈ T }) x with
          | ⟨F, hF⟩ =>
            Subtype.mk (p := fun (x : A) ↦ x ∈ T)
              (⋯.choose (p := fun (x : A) ↦ x ∈ T ∧ (↑F : IntermediateField ℚ A) = ℚ⟮x⟯)) ⋯ :
          { x : A // x ∈ T }))
      x_1)
⊢ (↑(↑x : { F : IntermediateField ℚ A // p F }) : IntermediateField ℚ A) =
    ℚ⟮⋯.choose (p := fun (x_2 : A) ↦
        x_2 ∈ T ∧ (↑(↑x : { F : IntermediateField ℚ A // p F }) : IntermediateField ℚ A) = ℚ⟮x_2⟯)⟯

Tactic:
exact (h _ (Subtype.mem _)).choose_spec.2

Premises used: Exists.choose_spec, And.right, Subtype.mem
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
A : Type u_2
inst : Field A
inst_1 : CharZero A
p : IntermediateField ℚ A → Prop
S : Set { F : IntermediateField ℚ A // p F }
T : Set A
hT : Finite.{u_2 + 1} (↑T : Type u_2)
h : ∀ F ∈ S, ∃ x ∈ T, (↑F : IntermediateField ℚ A) = ℚ⟮x⟯
x x_1 : (↑S : Type u_2)
h_eq :
  Eq.{u_2 + 1} (α := { x : A // x ∈ T })
    ((fun (x : (↑S : Type u_2)) ↦
        (match (motive := (↑S : Type u_2) → { x : A // x ∈ T }) x with
          | ⟨F, hF⟩ =>
            Subtype.mk (p := fun (x : A) ↦ x ∈ T)
              (⋯.choose (p := fun (x : A) ↦ x ∈ T ∧ (↑F : IntermediateField ℚ A) = ℚ⟮x⟯)) ⋯ :
          { x : A // x ∈ T }))
      x)
    ((fun (x : (↑S : Type u_2)) ↦
        (match (motive := (↑S : Type u_2) → { x : A // x ∈ T }) x with
          | ⟨F, hF⟩ =>
            Subtype.mk (p := fun (x : A) ↦ x ∈ T)
              (⋯.choose (p := fun (x : A) ↦ x ∈ T ∧ (↑F : IntermediateField ℚ A) = ℚ⟮x⟯)) ⋯ :
          { x : A // x ∈ T }))
      x_1)
⊢ (↑(↑x_1 : { F : IntermediateField ℚ A // p F }) : IntermediateField ℚ A) =
    ℚ⟮⋯.choose (p := fun (x : A) ↦
        x ∈ T ∧ (↑(↑x_1 : { F : IntermediateField ℚ A // p F }) : IntermediateField ℚ A) = ℚ⟮x⟯)⟯

Tactic:
(h _ (Subtype.mem _)).choose_spec.2

Premises used: Exists.choose_spec, And.right, Subtype.mem
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
A : Type u_2
inst : Field A
inst_1 : CharZero A
p : IntermediateField ℚ A → Prop
S : Set { F : IntermediateField ℚ A // p F }
T : Set A
hT : Finite.{u_2 + 1} (↑T : Type u_2)
h : ∀ F ∈ S, ∃ x ∈ T, (↑F : IntermediateField ℚ A) = ℚ⟮x⟯
x x_1 : (↑S : Type u_2)
h_eq :
  Eq.{u_2 + 1} (α := { x : A // x ∈ T })
    ((fun (x : (↑S : Type u_2)) ↦
        (match (motive := (↑S : Type u_2) → { x : A // x ∈ T }) x with
          | ⟨F, hF⟩ =>
            Subtype.mk (p := fun (x : A) ↦ x ∈ T)
              (⋯.choose (p := fun (x : A) ↦ x ∈ T ∧ (↑F : IntermediateField ℚ A) = ℚ⟮x⟯)) ⋯ :
          { x : A // x ∈ T }))
      x)
    ((fun (x : (↑S : Type u_2)) ↦
        (match (motive := (↑S : Type u_2) → { x : A // x ∈ T }) x with
          | ⟨F, hF⟩ =>
            Subtype.mk (p := fun (x : A) ↦ x ∈ T)
              (⋯.choose (p := fun (x : A) ↦ x ∈ T ∧ (↑F : IntermediateField ℚ A) = ℚ⟮x⟯)) ⋯ :
          { x : A // x ∈ T }))
      x_1)
⊢ (↑(↑x_1 : { F : IntermediateField ℚ A // p F }) : IntermediateField ℚ A) =
    ℚ⟮⋯.choose (p := fun (x : A) ↦
        x ∈ T ∧ (↑(↑x_1 : { F : IntermediateField ℚ A // p F }) : IntermediateField ℚ A) = ℚ⟮x⟯)⟯

Tactic:
exact (h _ (Subtype.mem _)).choose_spec.2

Premises used: Exists.choose_spec, And.right, Subtype.mem
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
⊢ N ≠ 0

Tactic:
fun h ↦ discr_ne_zero K ?_

Premises used: NumberField.discr_ne_zero, Not
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
refine : ∀ (h : N = 0), discr K = 0
⊢ N ≠ 0

Tactic:
refine fun h ↦ discr_ne_zero K ?_

Premises used: NumberField.discr_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h : N = 0
rwa : ∀ (hK : |discr K| ≤ (↑0 : ℤ)) (h : N = 0), discr K = 0
rwa₁ : ∀ (hK : |discr K| ≤ 0) (h : N = 0), discr K = 0
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (hK : discr K = 0) (h : N = 0), discr K = 0
⊢ discr K = 0

Tactic:
rwa [h, Nat.cast_zero, abs_nonpos_iff] at hK

Premises used: abs_nonpos_iff, Nat.cast_zero
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
⊢ N ≠ 0

Tactic:
have h_nz : N ≠ 0 := by
    refine fun h ↦ discr_ne_zero K ?_
    rwa [h, Nat.cast_zero, abs_nonpos_iff] at hK
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
⊢ LT.lt (α := ℝ) 0 4

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
⊢ LT.lt (α := ℝ) 0 3

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
rw : 4 / 3 < π
⊢ 1 < 3 * π / 4

Tactic:
rw [_root_.lt_div_iff₀ (by positivity), ← _root_.div_lt_iff₀' (by positivity), one_mul]

Premises used: lt_div_iff₀, div_lt_iff₀', one_mul
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
linarith : π ≤ 4 / 3 → 3 / 3 = 1
linarith₁ : π ≤ 4 / 3 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : π ≤ 4 / 3 → GT.gt (α := ℝ) 3 0
linarith₃ : π ≤ 4 / 3 → HMul.hMul (α := ℝ) 5 (-1) + (3 * π - HMul.hMul (α := ℝ) 1 4) + 3 * (3 - π) = 0
linarith₄ : π ≤ 4 / 3 → GT.gt (α := ℝ) 5 0
linarith₅ : π ≤ 4 / 3 → GT.gt (α := ℝ) 3 0
⊢ 4 / 3 < π

Tactic:
linarith [Real.pi_gt_three]

Premises used: Real.pi_gt_three
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
⊢ 1 < 3 * π / 4

Tactic:
have h₂ : 1 < 3 * π / 4 := by
    rw [_root_.lt_div_iff₀ (by positivity), ← _root_.div_lt_iff₀' (by positivity), one_mul]
    linarith [Real.pi_gt_three]
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
inl : ∀ (h : 1 < finrank ℚ K), finrank ℚ K ≤ rankOfDiscrBdd N
inr : ∀ (h : finrank ℚ K ≤ 1), finrank ℚ K ≤ rankOfDiscrBdd N
⊢ finrank ℚ K ≤ rankOfDiscrBdd N

Tactic:
obtain h | h := lt_or_ge 1 (finrank ℚ K)

Premises used: Rat, lt_or_ge, OfNat.ofNat, Module.finrank
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
inl : finrank ℚ K ≤ ⌊Real.log (9 / 4 * (↑N : ℝ)) / Real.log (3 * π / 4)⌋₊
⊢ finrank ℚ K ≤ rankOfDiscrBdd N

Tactic:
apply le_max_of_le_right

Premises used: le_max_of_le_right
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
inl : (↑(finrank ℚ K) : ℝ) ≤ Real.log (9 / 4 * (↑N : ℝ)) / Real.log (3 * π / 4)
inl₁ : 0 ≤ Real.log (9 / 4 * (↑N : ℝ)) / Real.log (3 * π / 4)
⊢ finrank ℚ K ≤ ⌊Real.log (9 / 4 * (↑N : ℝ)) / Real.log (3 * π / 4)⌋₊

Tactic:
rw [Nat.le_floor_iff]

Premises used: Nat.le_floor_iff
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
⊢ 4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤ (↑(↑N : ℤ) : ℝ)

Tactic:
have h := le_trans (abs_discr_ge h) (Int.cast_le.mpr hK)
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h_1 : 1 < finrank ℚ K
h : 4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤ (↑(↑N : ℤ) : ℝ)
inl :
  ∀ (h : Real.log (9 / 4 * (↑N : ℝ)) / Real.log (3 * π / 4) < (↑(finrank ℚ K) : ℝ)),
    (↑(↑N : ℤ) : ℝ) < 4 / 9 * (3 * π / 4) ^ finrank ℚ K
⊢ (↑(finrank ℚ K) : ℝ) ≤ Real.log (9 / 4 * (↑N : ℝ)) / Real.log (3 * π / 4)

Tactic:
contrapose! h
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h_1 : 1 < finrank ℚ K
h : Real.log (9 / 4 * (↑N : ℝ)) / Real.log (3 * π / 4) < (↑(finrank ℚ K) : ℝ)
inl : (↑(↑N : ℤ) : ℝ) < 4 / 9 * HPow.hPow (β := ℝ) (3 * π / 4) (↑(finrank ℚ K) : ℝ)
⊢ (↑(↑N : ℤ) : ℝ) < 4 / 9 * (3 * π / 4) ^ finrank ℚ K

Tactic:
rw [← Real.rpow_natCast]

Premises used: Real.rpow_natCast
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h_1 : 1 < finrank ℚ K
h : Real.log (9 / 4 * (↑N : ℝ)) / Real.log (3 * π / 4) < (↑(finrank ℚ K) : ℝ)
⊢ Real.logb (3 * π / 4) (9 / 4 * (↑N : ℝ)) < (↑(finrank ℚ K) : ℝ)

Tactic:
rw [Real.log_div_log] at h

Premises used: Real.log_div_log
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h_1 : 1 < finrank ℚ K
h : Real.logb (3 * π / 4) (9 / 4 * (↑N : ℝ)) < (↑(finrank ℚ K) : ℝ)
⊢ 0 < 4 / 9

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h_1 : 1 < finrank ℚ K
h : Real.logb (3 * π / 4) (9 / 4 * (↑N : ℝ)) < (↑(finrank ℚ K) : ℝ)
inl : (↑(↑N : ℤ) : ℝ) ≤ 4 / 9 * (3 * π / 4) ^ Real.logb (3 * π / 4) (9 / 4 * (↑N : ℝ))
⊢ (↑(↑N : ℤ) : ℝ) < 4 / 9 * HPow.hPow (β := ℝ) (3 * π / 4) (↑(finrank ℚ K) : ℝ)

Tactic:
refine lt_of_le_of_lt ?_ (mul_lt_mul_of_pos_left
        (Real.rpow_lt_rpow_of_exponent_lt h₂ h) (by positivity : (0 : ℝ) < 4 / 9))

Premises used: lt_of_le_of_lt, mul_lt_mul_of_pos_left, Real.rpow_lt_rpow_of_exponent_lt
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h_1 : 1 < finrank ℚ K
h : Real.logb (3 * π / 4) (9 / 4 * (↑N : ℝ)) < (↑(finrank ℚ K) : ℝ)
⊢ 0 < 9 / 4 * (↑N : ℝ)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h_1 : 1 < finrank ℚ K
h : Real.logb (3 * π / 4) (9 / 4 * (↑N : ℝ)) < (↑(finrank ℚ K) : ℝ)
⊢ 9 / 4 ≠ 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h_1 : 1 < finrank ℚ K
h : Real.logb (3 * π / 4) (9 / 4 * (↑N : ℝ)) < (↑(finrank ℚ K) : ℝ)
inl : (↑(↑N : ℤ) : ℝ) ≤ 4 / 9 * (9 / 4 * (↑N : ℝ))
inl₁ : (↑(↑N : ℤ) : ℝ) ≤ 4 / 9 * (9 / 4) * (↑N : ℝ)
inl₂ : (↑(↑N : ℤ) : ℝ) ≤ (9 / 4)⁻¹ * (9 / 4) * (↑N : ℝ)
inl₃ : (↑(↑N : ℤ) : ℝ) ≤ HMul.hMul (α := ℝ) 1 (↑N : ℝ)
inl₄ : LE.le (α := ℝ) (↑(↑N : ℤ) : ℝ) (↑N : ℝ)
inl₅ inl₆ : LE.le (α := ℝ) (↑N : ℝ) (↑N : ℝ)
⊢ (↑(↑N : ℤ) : ℝ) ≤ 4 / 9 * (3 * π / 4) ^ Real.logb (3 * π / 4) (9 / 4 * (↑N : ℝ))

Tactic:
rw [Real.rpow_logb (lt_trans zero_lt_one h₂) (ne_of_gt h₂) (by positivity), ← mul_assoc,
            ← inv_div, inv_mul_cancel₀ (by simp), one_mul, Int.cast_natCast]

Premises used: Int.cast_natCast, mul_assoc, lt_trans, ne_of_gt, Real.rpow_logb, zero_lt_one, inv_div, inv_mul_cancel₀, one_mul
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
⊢ 0 ≤ Real.log (9 / 4 * (↑N : ℝ)) / Real.log (3 * π / 4)

Tactic:
div_nonneg (Real.log_nonneg ?_) (Real.log_nonneg (le_of_lt h₂))

Premises used: le_of_lt, Real.log_nonneg, div_nonneg
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
inl : 1 ≤ 9 / 4 * (↑N : ℝ)
⊢ 0 ≤ Real.log (9 / 4 * (↑N : ℝ)) / Real.log (3 * π / 4)

Tactic:
refine div_nonneg (Real.log_nonneg ?_) (Real.log_nonneg (le_of_lt h₂))

Premises used: le_of_lt, Real.log_nonneg, div_nonneg
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
⊢ LT.lt (α := ℝ) 0 4

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
⊢ LT.lt (α := ℝ) 0 9

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
inl : 4 / 9 ≤ (↑N : ℝ)
⊢ 1 ≤ 9 / 4 * (↑N : ℝ)

Tactic:
rw [mul_comm, ← mul_div_assoc, _root_.le_div_iff₀ (by positivity), one_mul,
        ← _root_.div_le_iff₀ (by positivity)]

Premises used: div_le_iff₀, mul_div_assoc, mul_comm, le_div_iff₀, one_mul
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
⊢ 4 / 9 ≤ 1

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
⊢ 4 / 9 ≤ (↑N : ℝ)

Tactic:
exact le_trans (by norm_num) (Nat.one_le_cast.mpr (Nat.one_le_iff_ne_zero.mpr h_nz))

Premises used: Iff.mpr, Nat.one_le_cast, Nat.one_le_iff_ne_zero, le_trans
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : finrank ℚ K ≤ 1
⊢ finrank ℚ K ≤ rankOfDiscrBdd N

Tactic:
le_max_of_le_left h

Premises used: le_max_of_le_left
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : finrank ℚ K ≤ 1
⊢ finrank ℚ K ≤ rankOfDiscrBdd N

Tactic:
exact le_max_of_le_left h

Premises used: le_max_of_le_left