chore: replace Quotient.exists_rep with induction (#12471)

Following my advice [on Zulip](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/getting.20witness.20for.20points.20in.20the.20quotient/near/435785862); let's change more code to use `induction` so that users learning by example learn a better approach.

This is not exhaustive.

Mathlib/Algebra/Module/LocalizedModule.lean

@@ -430,14 +430,12 @@ theorem smul'_mk (r : R) (s : S) (m : M) : r • mk m s = mk (r • m) s := by
 
 theorem smul'_mul {A : Type*} [Semiring A] [Algebra R A] (x : T) (p₁ p₂ : LocalizedModule S A) :
     x • p₁ * p₂ = x • (p₁ * p₂) := by
-  obtain ⟨⟨a₁, s₁⟩, rfl : mk a₁ s₁ = p₁⟩ := Quotient.exists_rep p₁
-  obtain ⟨⟨a₂, s₂⟩, rfl : mk a₂ s₂ = p₂⟩ := Quotient.exists_rep p₂
+  induction p₁, p₂ using induction_on₂ with | _ a₁ s₁ a₂ s₂ => _
   rw [mk_mul_mk, smul_def, smul_def, mk_mul_mk, mul_assoc, smul_mul_assoc]
 
 theorem mul_smul' {A : Type*} [Semiring A] [Algebra R A] (x : T) (p₁ p₂ : LocalizedModule S A) :
     p₁ * x • p₂ = x • (p₁ * p₂) := by
-  obtain ⟨⟨a₁, s₁⟩, rfl : mk a₁ s₁ = p₁⟩ := Quotient.exists_rep p₁
-  obtain ⟨⟨a₂, s₂⟩, rfl : mk a₂ s₂ = p₂⟩ := Quotient.exists_rep p₂
+  induction p₁, p₂ using induction_on₂ with | _ a₁ s₁ a₂ s₂ => _
   rw [smul_def, mk_mul_mk, mk_mul_mk, smul_def, mul_left_comm, mul_smul_comm]
 
 variable (T)
@@ -469,13 +467,13 @@ noncomputable instance algebra' {A : Type*} [Semiring A] [Algebra R A] :
     show Module R (LocalizedModule S A) by infer_instance with
     commutes' := by
       intro r x
-      obtain ⟨⟨a, s⟩, rfl : mk a s = x⟩ := Quotient.exists_rep x
+      induction x using induction_on with | _ a s => _
       dsimp
       rw [← Localization.mk_one_eq_algebraMap, algebraMap_mk, mk_mul_mk, mk_mul_mk, mul_comm,
         Algebra.commutes]
     smul_def' := by
       intro r x
-      obtain ⟨⟨a, s⟩, rfl : mk a s = x⟩ := Quotient.exists_rep x
+      induction x using induction_on with | _ a s => _
       dsimp
       rw [← Localization.mk_one_eq_algebraMap, algebraMap_mk, mk_mul_mk, smul'_mk,
         Algebra.smul_def, one_mul] }

Mathlib/Combinatorics/Enumerative/Partition.lean

@@ -79,7 +79,7 @@ def ofComposition (n : ℕ) (c : Composition n) : Partition n where
 
 theorem ofComposition_surj {n : ℕ} : Function.Surjective (ofComposition n) := by
   rintro ⟨b, hb₁, hb₂⟩
-  rcases Quotient.exists_rep b with ⟨b, rfl⟩
+  induction b using Quotient.inductionOn with | _ b => ?_
   exact ⟨⟨b, hb₁, by simpa using hb₂⟩, Partition.ext _ _ rfl⟩
 #align nat.partition.of_composition_surj Nat.Partition.ofComposition_surj
 

Mathlib/GroupTheory/Perm/Sign.lean

@@ -339,7 +339,7 @@ theorem signAux3_mul_and_swap [Finite α] (f g : Perm α) (s : Multiset α) (hs
     signAux3 (f * g) hs = signAux3 f hs * signAux3 g hs ∧
       Pairwise fun x y => signAux3 (swap x y) hs = -1 := by
   obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin α
-  obtain ⟨l, rfl⟩ := Quotient.exists_rep s
+  induction s using Quotient.inductionOn with | _ l => ?_
   show
     signAux2 l (f * g) = signAux2 l f * signAux2 l g ∧
     Pairwise fun x y => signAux2 l (swap x y) = -1

Mathlib/Order/Filter/Germ.lean

@@ -287,7 +287,7 @@ and a function `g : γ → α` tends to `l` along `lc : Filter γ`,
 the germ of the composition `f ∘ g` is also constant. -/
 lemma isConstant_compTendsto {f : Germ l β} {lc : Filter γ} {g : γ → α}
     (hf : f.IsConstant) (hg : Tendsto g lc l) : (f.compTendsto g hg).IsConstant := by
-  rcases Quotient.exists_rep f with ⟨f, rfl⟩
+  induction f using Quotient.inductionOn with | _ f => ?_
   exact isConstant_comp_tendsto hf hg
 
 @[simp, norm_cast]