-- Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean
theorem _root_.NumberField.finite_of_discr_bdd :
    {K : { F : IntermediateField ℚ A // FiniteDimensional ℚ F} |
      haveI :  NumberField K := @NumberField.mk _ _ inferInstance K.prop
      |discr K| ≤ N }.Finite

Proof state:
case mk
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
hK₁ : ⟨K, hK₀⟩ ∈ {K | |discr ↥↑K| ≤ ↑N}
this✝ : CharZero ↥K
this : NumberField ↥K
⊢ ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N} ∪ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}

Tactic:
obtain ⟨w₀⟩ := (inferInstance : Nonempty (InfinitePlace K))

Result:
case mk.intro
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
hK₁ : ⟨K, hK₀⟩ ∈ {K | |discr ↥↑K| ≤ ↑N}
this✝ : CharZero ↥K
this : NumberField ↥K
w₀ : InfinitePlace ↥K
⊢ ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N} ∪ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}

Proof state:
case neg.a
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
hK₁ : ⟨K, hK₀⟩ ∈ {K | |discr ↥↑K| ≤ ↑N}
this✝ : CharZero ↥K
this : NumberField ↥K
w₀ : InfinitePlace ↥K
hw₀ : ¬w₀.IsReal
⊢ ⟨K, hK₀⟩ ∈ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}

Tactic:
exact ⟨⟨w₀, not_isReal_iff_isComplex.mp hw₀⟩, hK₁⟩

Result:
no goals

Proof state:
case pos.a
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
hK₁ : ⟨K, hK₀⟩ ∈ {K | |discr ↥↑K| ≤ ↑N}
this✝ : CharZero ↥K
this : NumberField ↥K
w₀ : InfinitePlace ↥K
hw₀ : w₀.IsReal
⊢ ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}

Tactic:
exact ⟨⟨w₀, hw₀⟩, hK₁⟩

Result:
no goals

Proof state:
case pos
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
hK₁ : ⟨K, hK₀⟩ ∈ {K | |discr ↥↑K| ≤ ↑N}
this✝ : CharZero ↥K
this : NumberField ↥K
w₀ : InfinitePlace ↥K
hw₀ : w₀.IsReal
⊢ ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N} ∪ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}

Tactic:
apply Set.mem_union_left

Result:
case pos.a
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
hK₁ : ⟨K, hK₀⟩ ∈ {K | |discr ↥↑K| ≤ ↑N}
this✝ : CharZero ↥K
this : NumberField ↥K
w₀ : InfinitePlace ↥K
hw₀ : w₀.IsReal
⊢ ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}

Proof state:
case mk.intro
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
hK₁ : ⟨K, hK₀⟩ ∈ {K | |discr ↥↑K| ≤ ↑N}
this✝ : CharZero ↥K
this : NumberField ↥K
w₀ : InfinitePlace ↥K
⊢ ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N} ∪ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}

Tactic:
by_cases hw₀ : IsReal w₀

Result:
case pos
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
hK₁ : ⟨K, hK₀⟩ ∈ {K | |discr ↥↑K| ≤ ↑N}
this✝ : CharZero ↥K
this : NumberField ↥K
w₀ : InfinitePlace ↥K
hw₀ : w₀.IsReal
⊢ ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N} ∪ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}

case neg
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
hK₁ : ⟨K, hK₀⟩ ∈ {K | |discr ↥↑K| ≤ ↑N}
this✝ : CharZero ↥K
this : NumberField ↥K
w₀ : InfinitePlace ↥K
hw₀ : ¬w₀.IsReal
⊢ ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N} ∪ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}

Proof state:
case neg
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
hK₁ : ⟨K, hK₀⟩ ∈ {K | |discr ↥↑K| ≤ ↑N}
this✝ : CharZero ↥K
this : NumberField ↥K
w₀ : InfinitePlace ↥K
hw₀ : ¬w₀.IsReal
⊢ ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N} ∪ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}

Tactic:
apply Set.mem_union_right

Result:
case neg.a
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
hK₁ : ⟨K, hK₀⟩ ∈ {K | |discr ↥↑K| ≤ ↑N}
this✝ : CharZero ↥K
this : NumberField ↥K
w₀ : InfinitePlace ↥K
hw₀ : ¬w₀.IsReal
⊢ ⟨K, hK₀⟩ ∈ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}

Proof state:
case mk
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
hK₁ : ⟨K, hK₀⟩ ∈ {K | |discr ↥↑K| ≤ ↑N}
this : CharZero ↥K
⊢ ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N} ∪ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}

Tactic:
haveI : NumberField K := @NumberField.mk _ _ inferInstance hK₀

Result:
case mk
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
hK₁ : ⟨K, hK₀⟩ ∈ {K | |discr ↥↑K| ≤ ↑N}
this✝ : CharZero ↥K
this : NumberField ↥K
⊢ ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N} ∪ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}

Proof state:
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
⊢ {K | |discr ↥↑K| ≤ ↑N}.Finite

Tactic:
refine Set.Finite.subset (Set.Finite.union (finite_of_discr_bdd_of_isReal A N)
  (finite_of_discr_bdd_of_isComplex A N)) ?_

Result:
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
⊢ {K | |discr ↥↑K| ≤ ↑N} ⊆
    {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N} ∪ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}

Proof state:
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
⊢ {K | |discr ↥↑K| ≤ ↑N} ⊆
    {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N} ∪ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}

Tactic:
rintro ⟨K, hK₀⟩ hK₁

Result:
case mk
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
hK₁ : ⟨K, hK₀⟩ ∈ {K | |discr ↥↑K| ≤ ↑N}
⊢ ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N} ∪ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}

Proof state:
case mk
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
hK₁ : ⟨K, hK₀⟩ ∈ {K | |discr ↥↑K| ≤ ↑N}
⊢ ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N} ∪ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}

Tactic:
have : CharZero K := SubsemiringClass.instCharZero K

Result:
case mk
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
hK₁ : ⟨K, hK₀⟩ ∈ {K | |discr ↥↑K| ≤ ↑N}
this : CharZero ↥K
⊢ ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N} ∪ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}