simp only at hy
case intro.intro.intro.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
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
ha : a ≠ 0
this : Fact (↑p).Prime := { out := hp }
n : ℤ
h0 : n ≠ 0
f : CyclotomicIntegers ↑p
Hf : ↑n = a * f
hy : (fun x => f • x) (a • g + ↑y) = (fun x => f • x) 0
⊢ False
case intro.intro.intro.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
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
ha : a ≠ 0
this : Fact (↑p).Prime := { out := hp }
n : ℤ
h0 : n ≠ 0
f : CyclotomicIntegers ↑p
Hf : ↑n = a * f
hy : f • (a • g + ↑y) = f • 0
⊢ False