kebekus
/
nevanlinna
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update stronglyMeromorphic.lean

This commit is contained in:
Stefan Kebekus 2024-10-23 13:31:22 +02:00
parent d80894ea6f
commit e7ca812ad8
1 changed files with 6 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
Nevanlinna/stronglyMeromorphic.lean
View File

@ -168,8 +168,12 @@ theorem StronglyMeromorphicAt_of_makeStronglyMeromorphic
exact h₃g exact h₃g
· unfold MeromorphicAt.makeStronglyMeromorphicAt · unfold MeromorphicAt.makeStronglyMeromorphicAt
simp simp
by_cases h₃f : hf.order = 0 by_cases h₃f : hf.order = (0 : ℤ)
· simp [h₃f] · let h₄f := (hf.order_eq_int_iff 0).1 h₃f
let G := Classical.choose h₄f
simp [h₃f]
let hG := Classical.choose_spec h₄f
simp at hG
sorry sorry
· simp [h₃f] · simp [h₃f]