diff --git a/Nevanlinna/harmonicAt.lean b/Nevanlinna/harmonicAt.lean
index 76d9f0d..7c16a62 100644
--- a/Nevanlinna/harmonicAt.lean
+++ b/Nevanlinna/harmonicAt.lean
@@ -22,7 +22,7 @@ theorem HarmonicAt_iff
   HarmonicAt f x ↔ ∃ s : Set ℂ, IsOpen s ∧ x ∈ s ∧ (ContDiffOn ℝ 2 f s) ∧ (∀ z ∈ s, Δ f z = 0) := by
   constructor
   · intro hf
-    obtain ⟨s₁, h₁s₁, h₂s₁, h₃s₁⟩ := hf.1.contDiffOn' le_rfl
+    obtain ⟨s₁, h₁s₁, h₂s₁, h₃s₁⟩ := hf.1.contDiffOn' le_rfl (by trivial)
     simp at h₃s₁
     obtain ⟨t₂, h₁t₂, h₂t₂⟩ := (Filter.eventuallyEq_iff_exists_mem.1 hf.2)
     obtain ⟨s₂, h₁s₂, h₂s₂, h₃s₂⟩ := mem_nhds_iff.1 h₁t₂
@@ -261,7 +261,7 @@ theorem harmonicAt_comp_CLM_is_harmonicAt
     apply ContDiffAt.continuousLinearMap_comp
     exact h.1
   · -- Δ (⇑l ∘ f) =ᶠ[nhds z] 0
-    obtain ⟨r, h₁r, h₂r⟩ := h.1.contDiffOn le_rfl
+    obtain ⟨r, h₁r, h₂r⟩ := h.1.contDiffOn le_rfl (by trivial)
     obtain ⟨s, h₁s, h₂s, h₃s⟩ := mem_nhds_iff.1 h₁r
     obtain ⟨t, h₁t, h₂t⟩ := Filter.eventuallyEq_iff_exists_mem.1 h.2
     obtain ⟨u, h₁u, h₂u, h₃u⟩ := mem_nhds_iff.1 h₁t