chore(Data/Finset/PiInduction): remove porting note about `clear_valu…

…e` (#12100) This tactic now exists.
leanprover-community · Apr 12, 2024 · cd0e7a0 · cd0e7a0
1 parent 72721e3
commit cd0e7a0
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/Mathlib/Data/Finset/PiInduction.lean b/Mathlib/Data/Finset/PiInduction.lean
@@ -49,8 +49,7 @@ theorem induction_on_pi_of_choice (r : ∀ i, α i → Finset (α i) → Prop)
   · rcases sigma_nonempty.1 hne with ⟨i, -, hi⟩
     rcases H_ex i (f i) hi with ⟨x, x_mem, hr⟩
     set g := update f i ((f i).erase x) with hg
--- Porting note: this tactic does not exist yet
---  clear_value g
+    clear_value g
     have hx' : x ∉ g i := by
       rw [hg, update_same]
       apply not_mem_erase