fix: Balloon.lean・Rank.lean の解消不能な overlappingInstances 警告を明示的に抑制

`Frame.IsBalloon`・`Frame.IsTree` は，親クラス（`IsStrictTotalOrder`・`IsTransitive`）
のインスタンスを型を書くために先に明示指定する必要があり，`extends`で束ねられた
インスタンスと構造的に重複してしまう．`omit`は`def`/`instance`や，型が依存変数を
参照する`lemma`には効かず，`variable`側から外すと広範囲の宣言に影響するため，
該当宣言にのみ`set_option linter.overlappingInstances false in`を付与し，
理由をコメントで明記した．意味・シグネチャは不変．

Co-Authored-By: Claude <noreply@anthropic.com>

Author: SnO2WMaN

Foundation/Modal/Kripke/Balloon.lean

@@ -18,9 +18,13 @@ open Formula.Kripke
 
 variable {F : Frame} [IsStrictTotalOrder _ F] {e : Cluster F} [F.IsBalloon e] {x : F.World} {φ : Formula ℕ}
 
+-- `[IsStrictTotalOrder _ F]` must be given explicitly before `e : Cluster F` can even be stated,
+-- so it cannot avoid overlapping with the `IsStrictTotalOrder` bundled inside `[F.IsBalloon e]`.
+set_option linter.overlappingInstances false in
 /-- Every points in enverope is reflexive. -/
 lemma rfl_in_envelope (hx : x ∈ e) : x ≺ x := Cluster.refl_of_mem_non_degenerate (envelope_non_degenerated) hx
 
+set_option linter.overlappingInstances false in
 /-- Every point in balloon can see all points in envelope. -/
 lemma covered_in_envelope (x : F.World) : ∀ t ∈ e, x ≺ t := by
   obtain ⟨t₁, rfl⟩ := Quotient.exists_rep e;
@@ -41,6 +45,7 @@ lemma covered_in_envelope (x : F.World) : ∀ t ∈ e, x ≺ t := by
     . have := IsTerminated.direct_terminated_of_trans (F := F.strictSkelteon) (t := ⟦t₁⟧) ⟦x⟧ ext₁;
       exact _root_.trans this.1 Rt₁₂;
 
+set_option linter.overlappingInstances false in
 /-- Every points from enverope is in enverope. -/
 lemma in_envelope_of_in_envelope (hx : x ∈ e) : ∀ {y}, x ≺ y → y ∈ e := by
   obtain ⟨t, rfl⟩ := Quotient.exists_rep e;
@@ -66,6 +71,9 @@ end Frame.IsBalloon
 lemma farthermost_point_of_not_box {M : Kripke.Model} [IsStrictOrder _ M.toFrame] {x : M} (h : ¬x ⊧ □φ) : ∃ y, x ≺ y ∧ ¬y ⊧ φ ∧ y ⊧ □φ := by
   sorry;
 
+-- `[F.IsTransitive]` is a required prior argument of the `Frame.IsBalloon` class itself,
+-- so it cannot avoid overlapping with the `IsTransitive` bundled inside `[F.IsBalloon e]`.
+set_option linter.overlappingInstances false in
 open
   Formula.Kripke
   Frame.IsBalloon

Foundation/Modal/Kripke/Rank.lean

@@ -181,6 +181,9 @@ namespace pointGenerate
 open Classical in
 instance : Fintype (F↾x) := by apply Subtype.fintype;
 
+-- the outer `variable [F.IsTransitive]` is needed by unrelated declarations in this section,
+-- so it cannot avoid overlapping with the `IsTransitive` bundled inside `[F.IsTree]` here.
+set_option linter.overlappingInstances false in
 instance [F.IsTree] : (F↾x).IsTree := by constructor;
 
 axiom eq_original_height (hxy : y = x ∨ x ≺ y) : Frame.rank (F := F↾x) (⟨y, hxy⟩) = Frame.rank y