Theorem: systemOfUnits.existence'' (FltRegular/NumberTheory/SystemOfUnits.lean)

State before:
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
hR : R ≤ r
⊢ Nonempty (systemOfUnits p G R)
Tactic:
induction R with
| zero => exact existence0 p G
| succ n ih =>
    obtain ⟨S⟩ := ih (le_trans (Nat.le_succ n) hR)
    exact existence' p hp G r hf S (lt_of_lt_of_le (Nat.lt.base n) hR)
State after:
no goals

State before:
case zero
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
hR : 0 ≤ r
⊢ Nonempty (systemOfUnits p G 0)
Tactic:
exact existence0 p G
State after:
no goals

State before:
case succ
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
n : ℕ
ih : n ≤ r → Nonempty (systemOfUnits p G n)
hR : n + 1 ≤ r
⊢ Nonempty (systemOfUnits p G (n + 1))
Tactic:
obtain ⟨S⟩ := ih (le_trans (Nat.le_succ n) hR)
State after:
case succ.intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
n : ℕ
ih : n ≤ r → Nonempty (systemOfUnits p G n)
hR : n + 1 ≤ r
S : systemOfUnits p G n
⊢ Nonempty (systemOfUnits p G (n + 1))

State before:
case succ.intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
n : ℕ
ih : n ≤ r → Nonempty (systemOfUnits p G n)
hR : n + 1 ≤ r
S : systemOfUnits p G n
⊢ Nonempty (systemOfUnits p G (n + 1))
Tactic:
exact existence' p hp G r hf S (lt_of_lt_of_le (Nat.lt.base n) hR)
State after:
no goals