diff --git a/RMT4.lean b/RMT4.lean
index 22398a1..5b385bf 100644
--- a/RMT4.lean
+++ b/RMT4.lean
@@ -21,6 +21,8 @@ import RMT4.uniform
 
 open UniformConvergence Topology Filter Set Metric Function
 
+variable {ι : Type*} {l : Filter ι} {U : Set ℂ} {z₀ : ℂ}
+
 -- Anatole did this for Lean3 at https://github.com/leanprover-community/mathlib/pull/18017
 -- Lean4 port: https://github.com/leanprover-community/mathlib4/pull/6844
 instance : CompleteSpace (ℂ →ᵤ[compacts U] ℂ) := by sorry
diff --git a/RMT4/Covering.lean b/RMT4/Covering.lean
index acf0093..4a1fce6 100644
--- a/RMT4/Covering.lean
+++ b/RMT4/Covering.lean
@@ -10,14 +10,16 @@ variable {U : Set ℂ} {f : ℂ → ℂ} {Λ Λ' : LocalPrimitiveOn U f}
 
 namespace LocalPrimitiveOn
 
+variable {z w b1 : U} {u b2 w : ℂ} {a : U × ℂ}
+
 /-- The shift of `Λ.F z` going through a -/
 def FF (Λ : LocalPrimitiveOn U f) (z : U) (a : U × ℂ) (w : ℂ) : ℂ := Λ.F z w + (a.2 - Λ.F z a.1)
 
-@[simp] lemma FF_self : Λ.FF z (w, u) w = u := by simp [FF]
+@[simp] lemma FF_self {w : U} : Λ.FF z (w, u) w = u := by simp [FF]
 
-@[simp] lemma FF_self' : Λ.FF z w w.1 = w.2 := FF_self
+@[simp] lemma FF_self' {w : U × ℂ} : Λ.FF z w w.1 = w.2 := FF_self
 
-lemma FF_congr (h : Λ.FF z a (b1 : U) = b2) : Λ.FF z a = Λ.FF z (b1, b2) := by
+lemma FF_congr (h : Λ.FF z a b1 = b2) : Λ.FF z a = Λ.FF z (b1, b2) := by
   rw [← h] ; unfold FF ; simp
 
 lemma FF_deriv (hw : w ∈ Λ.S z) : HasDerivAt (Λ.FF z a) (f w) w := Λ.der z w hw |>.add_const _
@@ -31,7 +33,7 @@ theorem isOpen_FF_eq (Λ Λ' : LocalPrimitiveOn U f) (i j : U × ℂ) (i1 j1 : U
     eventually_of_mem (Λ.opn i1 |>.mem_nhds h1) (λ w => FF_deriv)
   have l2 : ∀ᶠ w in 𝓝 z, HasDerivAt (Λ'.FF j1 j) (f w) w :=
     eventually_of_mem (Λ'.opn j1 |>.mem_nhds h2) (λ w => FF_deriv)
-  have l4 := @eventuallyEq_of_hasDeriv ℂ _ f z (Λ.FF i1 i) (Λ'.FF j1 j) l1 l2 h3
+  have l4 := @eventuallyEq_of_hasDeriv ℂ _ f (Λ.FF i1 i) (Λ'.FF j1 j) z l1 l2 h3
   have l5 := inter_mem (inter_mem l4 (Λ.opn i1 |>.mem_nhds h1)) (Λ'.opn j1 |>.mem_nhds h2)
   exact ⟨_, l5, λ w _ h => ⟨⟨h.1.2, h.2⟩, h.1.1.symm⟩⟩
 
@@ -48,6 +50,8 @@ abbrev p (Λ : LocalPrimitiveOn U f) (z : covering Λ) : U := z.fst
 
 namespace covering
 
+variable {x a b : U} {s : Set (covering Λ)}
+
 /-- The shear transformation. `Φ z` maps a point `(u, v)` to `(u, w)` where `w` is the value above
   `z` of the translate of `F z` that goes through `(u, v)`, and `(Φ z).symm` maps `(u, w)` to
   `(u, v)` where `v` is the value above `u` of the translate of `F` that goes through `(z, v)`. -/
@@ -87,7 +91,8 @@ def nhd (z : covering Λ) : Filter (covering Λ) := nhd_from z.1 z
 lemma mem_nhd_from {z : covering Λ} : s ∈ nhd_from x z ↔ ∀ᶠ u in 𝓝 z.1, ⟨u, Λ.FF x z u⟩ ∈ s :=
   by rfl
 
-lemma titi1 (ha : z.1 ∈ Λ.S a) (hb : z.1 ∈ Λ'.S b) : ∀ᶠ u in 𝓝 z.1, Λ.FF a z u = Λ'.FF b z u := by
+lemma titi1 {z : U × ℂ} (ha : z.1.1 ∈ Λ.S a) (hb : z.1.1 ∈ Λ'.S b) :
+    ∀ᶠ u in 𝓝 z.1, Λ.FF a z u = Λ'.FF b z u := by
   -- let s := {z_1 : U | z_1 ∈ val ⁻¹' S Λ a ∩ val ⁻¹' S Λ' b ∧ FF Λ a z z_1 = FF Λ' b z z_1}
   -- have e1 : IsOpen s := @isOpen_FF_eq U f Λ Λ' z z a b
   -- have e2 : z.1 ∈ s := ⟨⟨ha, hb⟩, by simp only [FF_self']⟩
@@ -151,10 +156,12 @@ theorem isOpen_target : IsOpen (T_LocalEquiv Λ z).target := by
   simp [T_LocalEquiv, L]
   exact IsOpen.prod (isOpen_induced (Λ.opn z)) isOpen_univ
 
+variable {α β : Type*} {s : Set (α × β)} {t : Set α} {b : β}
+
 lemma toto10 (l : Filter α) (b : β) : s ∈ l ×ˢ pure b ↔ ∃ t ∈ l, t ×ˢ {b} ⊆ s := by
   simpa using exists_mem_subset_iff.symm
 
-lemma toto11 {s : Set (α × β)}: t ×ˢ {b} ⊆ s ↔ ∀ y ∈ t, (y, b) ∈ s where
+lemma toto11 {s : Set (α × β)} : t ×ˢ {b} ⊆ s ↔ ∀ y ∈ t, (y, b) ∈ s where
   mp h y hy := h ⟨hy, rfl⟩
   mpr h := by rintro ⟨y, b'⟩ ⟨hy, rfl⟩ ; exact h y hy
 
@@ -163,11 +170,12 @@ lemma toto12 [TopologicalSpace α] [TopologicalSpace β] [DiscreteTopology β] {
   rw [nhds_prod_eq, nhds_discrete β, toto10, eventually_iff_exists_mem]
   simp only [toto11]
 
-lemma toto13 {w : U × Λ.p ⁻¹' {z}} : s ∈ 𝓝 w ↔ ∀ᶠ x in 𝓝 w.1, (x, w.2) ∈ s := by
+lemma toto13 {s : Set (↑U × ↑(p Λ ⁻¹' {z}))} {w : U × Λ.p ⁻¹' {z}} :
+    s ∈ 𝓝 w ↔ ∀ᶠ x in 𝓝 w.1, (x, w.2) ∈ s := by
   have l1 : DiscreteTopology (Λ.p ⁻¹' {z}) := Bunch.discreteTopology
   exact toto12
 
-theorem toto9 (h : ↑w.1 ∈ Λ.S z) : ContinuousAt (T_LocalEquiv Λ z) w := by
+theorem toto9 {w : covering Λ} (h : ↑w.1 ∈ Λ.S z) : ContinuousAt (T_LocalEquiv Λ z) w := by
   rw [ContinuousAt, Tendsto]
   intro s hs
   rw [toto13] at hs
@@ -176,7 +184,8 @@ theorem toto9 (h : ↑w.1 ∈ Λ.S z) : ContinuousAt (T_LocalEquiv Λ z) w := by
   filter_upwards [hs] with x hx
   simpa [FF] using hx
 
-theorem toto9' (h : ↑w.1 ∈ Λ.S z) : ContinuousAt (T_LocalEquiv Λ z).symm w := by
+theorem toto9' {w : ↑U × ↑(p Λ ⁻¹' {z})} (h : ↑w.1 ∈ Λ.S z) :
+    ContinuousAt (T_LocalEquiv Λ z).symm w := by
   rw [ContinuousAt, Tendsto]
   intro s hs
   simp
diff --git a/RMT4/Glue.lean b/RMT4/Glue.lean
index 636916e..06dca73 100644
--- a/RMT4/Glue.lean
+++ b/RMT4/Glue.lean
@@ -2,9 +2,6 @@ import Mathlib.Topology.ContinuousFunction.Basic
 import Mathlib.Topology.MetricSpace.PseudoMetric
 import Mathlib.Topology.Algebra.Order.ProjIcc
 
-set_option autoImplicit false
-set_option pp.proofs.withType false
-
 open Set Interval
 
 variable {a b c t : ℝ} {E : Type*} [TopologicalSpace E]
diff --git a/RMT4/Lift.lean b/RMT4/Lift.lean
index ad5e54d..ac7be4c 100644
--- a/RMT4/Lift.lean
+++ b/RMT4/Lift.lean
@@ -4,9 +4,6 @@ import Mathlib.Topology.Covering
 import Mathlib.Topology.LocallyConstant.Basic
 import RMT4.Glue
 
-set_option autoImplicit false
-set_option pp.proofs.withType false
-
 open Set Topology Metric unitInterval Filter ContinuousMap
 
 variable {E X : Type*} [TopologicalSpace E] [TopologicalSpace X] {f : E → X}
diff --git a/RMT4/defs.lean b/RMT4/defs.lean
index fa53200..dd5cc06 100644
--- a/RMT4/defs.lean
+++ b/RMT4/defs.lean
@@ -3,7 +3,7 @@ import RMT4.deriv_inj
 
 open Complex Metric Set
 
--- variables {U V W : set ℂ}
+variable {u : ℂ} {U V W : Set ℂ}
 
 namespace RMT
 
@@ -88,4 +88,4 @@ lemma embedding.deriv_ne_zero {f : embedding U V} {z : ℂ} (hU : IsOpen U) (hz
   deriv f z ≠ 0 :=
 deriv_ne_zero_of_inj hU f.is_diff f.is_inj hz
 
-end RMT
\ No newline at end of file
+end RMT
diff --git a/RMT4/deriv_inj.lean b/RMT4/deriv_inj.lean
index 5ace333..8d873af 100644
--- a/RMT4/deriv_inj.lean
+++ b/RMT4/deriv_inj.lean
@@ -2,7 +2,7 @@ import RMT4.hurwitz
 
 open Complex Metric circleIntegral Topology Filter Set
 
-variable {U : Set ℂ}
+variable {ι α β : Type*} {U : Set ℂ} {c z₀ : ℂ} {r : ℝ} {f g : ℂ → ℂ}
 
 lemma crucial (hU : IsOpen U) (hcr : closedBall c r ⊆ U) (hz₀ : z₀ ∈ ball c r) (hf : DifferentiableOn ℂ f U)
     (hfz₀ : f z₀ = 0) (hf'z₀ : deriv f z₀ ≠ 0) (hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0) :
diff --git a/RMT4/etape2.lean b/RMT4/etape2.lean
index 6806769..b676c23 100644
--- a/RMT4/etape2.lean
+++ b/RMT4/etape2.lean
@@ -8,7 +8,7 @@ open Complex ComplexConjugate Set Metric Topology Filter
 
 namespace RMT
 
-variable (U : Set ℂ) [good_domain U]
+variable {z u z₀ : ℂ} (U : Set ℂ) [good_domain U]
 
 lemma one_sub_mul_conj_ne_zero (hu : u ∈ 𝔻) (hz : z ∈ 𝔻) : 1 - z * conj u ≠ 0 := by
   rw [mem_𝔻_iff] at hu hz
diff --git a/RMT4/montel.lean b/RMT4/montel.lean
index f7f257f..17600e7 100644
--- a/RMT4/montel.lean
+++ b/RMT4/montel.lean
@@ -7,7 +7,7 @@ open Set Function Metric UniformConvergence Complex
 
 def compacts (U : Set ℂ) : Set (Set ℂ) := {K | K ⊆ U ∧ IsCompact K}
 
-variable {ι : Type u} {F : ι → ℂ →ᵤ[compacts U] ℂ}
+variable {ι : Type*} {U K : Set ℂ} {z : ℂ} {F : ι → ℂ →ᵤ[compacts U] ℂ}
 
 @[simp] lemma union_compacts : ⋃₀ compacts U = U :=
   subset_antisymm (λ _ ⟨_, hK, hz⟩ => hK.1 hz)
diff --git a/RMT4/pintegral.lean b/RMT4/pintegral.lean
index 7b4acc6..29f1e6d 100644
--- a/RMT4/pintegral.lean
+++ b/RMT4/pintegral.lean
@@ -4,6 +4,8 @@ import RMT4.Subdivision
 
 open BigOperators Metric Set Subdivision Topology Filter Nat
 
+variable {s t U V : Set ℂ} {z z₀ : ℂ} {f F : ℂ → ℂ} {a b : ℝ} {γ : ℝ → ℂ} {n : ℕ}
+
 structure LocalPrimitiveOn (s : Set ℂ) (f : ℂ → ℂ) :=
   F : s → ℂ → ℂ
   S : s → Set ℂ
diff --git a/RMT4/square.lean b/RMT4/square.lean
index acd8949..bc4c0f4 100644
--- a/RMT4/square.lean
+++ b/RMT4/square.lean
@@ -1,7 +1,5 @@
 import Mathlib
 
-set_option autoImplicit false
-
 local notation "𝕀" => unitInterval
 
 open Complex
diff --git a/RMT4/square2.lean b/RMT4/square2.lean
index 163daff..a14fd3c 100644
--- a/RMT4/square2.lean
+++ b/RMT4/square2.lean
@@ -1,8 +1,6 @@
 import Mathlib
 import RMT4.Primitive
 
-set_option autoImplicit false
-
 variable {f f' F : ℂ → ℂ} {w z z₁ z₂ z₃ z₄ w₁ w₂ w₃ w₄ p : ℂ} {W : Fin 4 -> ℂ}
   {t x x₁ x₂ y y₁ y₂ : ℝ} {U : Set ℂ} {γ₁ γ₂ : ℝ → ℂ}