-- 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
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)
b : K →+* ℂ
this : a k' l * (NumberField.house.newBasis K) b = 0
⊢ a k' l = 0 k' l

Tactic:
simp only [mul_eq_zero] at this

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)
b : K →+* ℂ
this : a k' l = 0 ∨ (NumberField.house.newBasis K) b = 0
⊢ 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
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

Tactic:
let ⟨b⟩ := Fintype.card_pos_iff.1 (Fintype.card_pos (α := (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)
b : K →+* ℂ
⊢ 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
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)
b : K →+* ℂ
⊢ (NumberField.house.newBasis K).repr (a k' l * (NumberField.house.newBasis K) b) = 0

Tactic:
ext b'

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 : β
hs :
  ∀ (b : K →+* ℂ),
    (fun l => ((NumberField.house.newBasis K).repr (a k' l.1 * (NumberField.house.newBasis K) l.2)) b) = 0 (k', b)
b b' : K →+* ℂ
⊢ ((NumberField.house.newBasis K).repr (a k' l * (NumberField.house.newBasis K) b)) b' = 0 b'

Proof state:
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

Tactic:
intros 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 :
  ∀ (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

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)
⊢ ∀ (i : α) (j : β), a i j = 0 i j

Tactic:
intros k' l

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)
k' : α
l : β
⊢ 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
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)
b : K →+* ℂ
this : a k' l = 0 ∨ (NumberField.house.newBasis K) b = 0
⊢ a k' l = 0 k' l

Tactic:
exact this.resolve_right (Basis.ne_zero (newBasis K) b)

Result:
no goals

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 : β
hs :
  ∀ (b : K →+* ℂ),
    (fun l => ((NumberField.house.newBasis K).repr (a k' l.1 * (NumberField.house.newBasis K) l.2)) b) = 0 (k', b)
b b' : K →+* ℂ
⊢ ((NumberField.house.newBasis K).repr (a k' l * (NumberField.house.newBasis K) b)) b' = 0 b'

Tactic:
specialize hs b'

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 : (fun l => ((NumberField.house.newBasis K).repr (a k' l.1 * (NumberField.house.newBasis K) l.2)) b') = 0 (k', b')
⊢ ((NumberField.house.newBasis K).repr (a k' l * (NumberField.house.newBasis K) b)) b' = 0 b'

Proof state:
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)
b : K →+* ℂ
⊢ a k' l = 0 k' l

Tactic:
have := ((newBasis K).repr.map_eq_zero_iff (x := (a k' l * (newBasis K) b))).1 <| by
  ext b'
  specialize hs b'
  rw [funext_iff] at hs
  simp only [Prod.forall] at hs
  apply hs

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)
b : K →+* ℂ
this : a k' l * (NumberField.house.newBasis K) b = 0
⊢ 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)
⊢ a = 0

Tactic:
rw [← Matrix.ext_iff]

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)
⊢ ∀ (i : α) (j : β), a i j = 0 i j

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
⊢ NumberField.house.asiegel K a ≠ 0

Tactic:
simp (config := { unfoldPartialApp := true }) only [asiegel, a']

Result:
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

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 : (fun l => ((NumberField.house.newBasis K).repr (a k' l.1 * (NumberField.house.newBasis K) l.2)) b') = 0 (k', b')
⊢ ((NumberField.house.newBasis K).repr (a k' l * (NumberField.house.newBasis K) b)) b' = 0 b'

Tactic:
rw [funext_iff] 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 :
  ∀ (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'

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:
simp only [ne_eq]

Result:
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