-- Mathlib/NumberTheory/NumberField/House.lean
theorem asiegel_ne_0 : asiegel K a ≠ 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
hs :
  ∀ (a_1 : α) (b : K →+* ℂ),
    (fun l => ((NumberField.house.newBasis K).repr (a a_1 l.1 * (NumberField.house.newBasis K) l.2)) b) = 0 (a_1, b)
k' : α
l : β
⊢ a k' l = 0 k' l

Tactic:
specialize hs k'

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
k' : α
l : β
hs :
  ∀ (b : K →+* ℂ),
    (fun l => ((NumberField.house.newBasis K).repr (a k' l.1 * (NumberField.house.newBasis K) l.2)) b) = 0 (k', b)
⊢ a k' l = 0 k' l

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
hs :
  ∀ (a_1 : α) (b : K →+* ℂ),
    (fun l => ((NumberField.house.newBasis K).repr (a a_1 l.1 * (NumberField.house.newBasis K) l.2)) b) = 0 (a_1, b)
⊢ False

Tactic:
apply ha

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
hs :
  ∀ (a_1 : α) (b : K →+* ℂ),
    (fun l => ((NumberField.house.newBasis K).repr (a a_1 l.1 * (NumberField.house.newBasis K) l.2)) b) = 0 (a_1, b)
⊢ a = 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
hs :
  ∀ (x : α × (K →+* ℂ)),
    (fun l => ((NumberField.house.newBasis K).repr (a x.1 l.1 * (NumberField.house.newBasis K) l.2)) x.2) = 0 x
⊢ False

Tactic:
simp only [Prod.forall] at hs

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
hs :
  ∀ (a_1 : α) (b : K →+* ℂ),
    (fun l => ((NumberField.house.newBasis K).repr (a a_1 l.1 * (NumberField.house.newBasis K) l.2)) b) = 0 (a_1, b)
⊢ False

Proof state:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
k' : α
l : β
b b' : K →+* ℂ
hs :
  ∀ (x : β × (K →+* ℂ)),
    ((NumberField.house.newBasis K).repr (a k' x.1 * (NumberField.house.newBasis K) x.2)) b' = 0 (k', b') x
⊢ ((NumberField.house.newBasis K).repr (a k' l * (NumberField.house.newBasis K) b)) b' = 0 b'

Tactic:
simp only [Prod.forall] at hs

Result:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
k' : α
l : β
b b' : K →+* ℂ
hs :
  ∀ (a_1 : β) (b : K →+* ℂ),
    ((NumberField.house.newBasis K).repr (a k' a_1 * (NumberField.house.newBasis K) b)) b' = 0 (k', b') (a_1, b)
⊢ ((NumberField.house.newBasis K).repr (a k' l * (NumberField.house.newBasis K) b)) b' = 0 b'

Proof state:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
k' : α
l : β
b b' : K →+* ℂ
hs :
  ∀ (a_1 : β) (b : K →+* ℂ),
    ((NumberField.house.newBasis K).repr (a k' a_1 * (NumberField.house.newBasis K) b)) b' = 0 (k', b') (a_1, b)
⊢ ((NumberField.house.newBasis K).repr (a k' l * (NumberField.house.newBasis K) b)) b' = 0 b'

Tactic:
apply hs

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
⊢ ¬(fun k l => ((NumberField.house.newBasis K).repr (a k.1 l.1 * (NumberField.house.newBasis K) l.2)) k.2) = 0

Tactic:
rw [funext_iff]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
⊢ ¬∀ (x : α × (K →+* ℂ)),
      (fun l => ((NumberField.house.newBasis K).repr (a x.1 l.1 * (NumberField.house.newBasis K) l.2)) x.2) = 0 x