How does introv work?

Stream: new members

[Kenny Lau]

import Mathlib.Tactic

universe u

def foo : Prop :=
  ∀ ⦃R : Type u⦄ (S : Type u) [CommRing R] [CommRing S], R = S → S = R

theorem bar : foo.{u} := by
  introv R hR hS h
/-
R S : Type u
hR : CommRing R
hS : CommRing S
h : R = S
⊢ S = R
-/

example : ∀ a b : Nat, a = b → b = a := by
  introv h
/-
a b : ℕ
h : a = b
⊢ b = a
-/

[Kenny Lau]

I am very confused on how introv works. What's a dependent hypothesis?