Warning when working on a goal without fully solving it

Stream: new members

[Bbbbbbbbba]

This works but gives a linter warning, because intro hxC; have hxS := hC hxC only applies to one goal. However I could not focus on it because I do not fully solve it yet; the next all_goals line does the job.

import Mathlib

open symmDiff

variable {E : Type*} [Finite E]

example {A B C : Set E} (hC : C ⊆ A ∆ B) : C = (C ∩ A) ∆ (C ∩ B) := by
  ext x
  constructor
  intro hxC; have hxS := hC hxC
  all_goals by_cases x ∈ A <;> by_cases x ∈ B <;> simp_all [ Set.mem_symmDiff ]

[Jakub Nowak]

You can use the focus tactic I think?

[Bbbbbbbbba]

Oh you are right