Theorem: Finset.getUnique_eq (LeanSAT/Upstream/ToMathlib.lean)

State before:
α : Type u_1
xs : Finset α
h : ∃ x, xs = {x}
v : α
⊢ getUnique xs h = v ↔ xs = {v}
Tactic:
rcases h with ⟨x,rfl⟩
State after:
case intro
α : Type u_1
v x : α
⊢ getUnique {x} ⋯ = v ↔ {x} = {v}

State before:
case intro
α : Type u_1
v x : α
⊢ getUnique {x} ⋯ = v ↔ {x} = {v}
Tactic:
simp [getUnique]
State after:
case intro
α : Type u_1
v x : α
⊢ elim {x}
        (fun L _hL =>
          match L, _hL with
          | [], _hL => ⋯.elim
          | x_1 :: tail, _hL => x_1)
        ⋯ =
      v ↔
    x = v

State before:
case intro
α : Type u_1
v x : α
⊢ elim {x}
        (fun L _hL =>
          match L, _hL with
          | [], _hL => ⋯.elim
          | x_1 :: tail, _hL => x_1)
        ⋯ =
      v ↔
    x = v
Tactic:
apply elim_eq_forall
State after:
case intro.hmotive
α : Type u_1
v x : α
⊢ ∀ {L : List ?intro.α} {hL : ↑L = ?intro.s.val},
    elim ?intro.s ?intro.f ?intro.h = ?intro.f L hL →
      (elim {x}
            (fun L _hL =>
              match L, _hL with
              | [], _hL => ⋯.elim
              | x_1 :: tail, _hL => x_1)
            ⋯ =
          v ↔
        x = v)

case intro.α
α : Type u_1
v x : α
⊢ Type ?u.15504

case intro.β
α : Type u_1
v x : α
⊢ Type ?u.15505

case intro.s
α : Type u_1
v x : α
⊢ Finset ?intro.α

case intro.f
α : Type u_1
v x : α
⊢ (L : List ?intro.α) → ↑L = ?intro.s.val → ?intro.β

case intro.h
α : Type u_1
v x : α
⊢ ∀ (a b : List ?intro.α) (ha : ↑a = ?intro.s.val) (hb : ↑b = ?intro.s.val), ?intro.f a ha = ?intro.f b hb

State before:
case intro.hmotive
α : Type u_1
v x : α
⊢ ∀ {L : List ?intro.α} {hL : ↑L = ?intro.s.val},
    elim ?intro.s ?intro.f ?intro.h = ?intro.f L hL →
      (elim {x}
            (fun L _hL =>
              match L, _hL with
              | [], _hL => ⋯.elim
              | x_1 :: tail, _hL => x_1)
            ⋯ =
          v ↔
        x = v)

case intro.α
α : Type u_1
v x : α
⊢ Type ?u.15504

case intro.β
α : Type u_1
v x : α
⊢ Type ?u.15505

case intro.s
α : Type u_1
v x : α
⊢ Finset ?intro.α

case intro.f
α : Type u_1
v x : α
⊢ (L : List ?intro.α) → ↑L = ?intro.s.val → ?intro.β

case intro.h
α : Type u_1
v x : α
⊢ ∀ (a b : List ?intro.α) (ha : ↑a = ?intro.s.val) (hb : ↑b = ?intro.s.val), ?intro.f a ha = ?intro.f b hb
Tactic:
intro L hL heq
State after:
case intro.hmotive
α : Type u_1
v x : α
L : List ?intro.α
hL : ↑L = ?intro.s.val
heq : elim ?intro.s ?intro.f ?intro.h = ?intro.f L hL
⊢ elim {x}
        (fun L _hL =>
          match L, _hL with
          | [], _hL => ⋯.elim
          | x_1 :: tail, _hL => x_1)
        ⋯ =
      v ↔
    x = v

case intro.α
α : Type u_1
v x : α
⊢ Type ?u.15504

case intro.β
α : Type u_1
v x : α
⊢ Type ?u.15505

case intro.s
α : Type u_1
v x : α
⊢ Finset ?intro.α

case intro.f
α : Type u_1
v x : α
⊢ (L : List ?intro.α) → ↑L = ?intro.s.val → ?intro.β

case intro.h
α : Type u_1
v x : α
⊢ ∀ (a b : List ?intro.α) (ha : ↑a = ?intro.s.val) (hb : ↑b = ?intro.s.val), ?intro.f a ha = ?intro.f b hb

State before:
case intro.hmotive
α : Type u_1
v x : α
L : List ?intro.α
hL : ↑L = ?intro.s.val
heq : elim ?intro.s ?intro.f ?intro.h = ?intro.f L hL
⊢ elim {x}
        (fun L _hL =>
          match L, _hL with
          | [], _hL => ⋯.elim
          | x_1 :: tail, _hL => x_1)
        ⋯ =
      v ↔
    x = v

case intro.α
α : Type u_1
v x : α
⊢ Type ?u.15504

case intro.β
α : Type u_1
v x : α
⊢ Type ?u.15505

case intro.s
α : Type u_1
v x : α
⊢ Finset ?intro.α

case intro.f
α : Type u_1
v x : α
⊢ (L : List ?intro.α) → ↑L = ?intro.s.val → ?intro.β

case intro.h
α : Type u_1
v x : α
⊢ ∀ (a b : List ?intro.α) (ha : ↑a = ?intro.s.val) (hb : ↑b = ?intro.s.val), ?intro.f a ha = ?intro.f b hb
Tactic:
rw [heq]
State after:
case intro.hmotive
α : Type u_1
v x : α
L : List α
hL : ↑L = {x}.val
heq :
  elim {x}
      (fun L _hL =>
        match L, _hL with
        | [], _hL => ⋯.elim
        | x_1 :: tail, _hL => x_1)
      ⋯ =
    match L, hL with
    | [], _hL => ⋯.elim
    | x_1 :: tail, _hL => x_1
⊢ (match L, hL with
      | [], _hL => ⋯.elim
      | x_1 :: tail, _hL => x_1) =
      v ↔
    x = v

State before:
case intro.hmotive
α : Type u_1
v x : α
L : List α
hL : ↑L = {x}.val
heq :
  elim {x}
      (fun L _hL =>
        match L, _hL with
        | [], _hL => ⋯.elim
        | x_1 :: tail, _hL => x_1)
      ⋯ =
    match L, hL with
    | [], _hL => ⋯.elim
    | x_1 :: tail, _hL => x_1
⊢ (match L, hL with
      | [], _hL => ⋯.elim
      | x_1 :: tail, _hL => x_1) =
      v ↔
    x = v
Tactic:
clear heq
State after:
case intro.hmotive
α : Type u_1
v x : α
L : List α
hL : ↑L = {x}.val
⊢ (match L, hL with
      | [], _hL => ⋯.elim
      | x_1 :: tail, _hL => x_1) =
      v ↔
    x = v

State before:
case intro.hmotive
α : Type u_1
v x : α
L : List α
hL : ↑L = {x}.val
⊢ (match L, hL with
      | [], _hL => ⋯.elim
      | x_1 :: tail, _hL => x_1) =
      v ↔
    x = v
Tactic:
simp at hL
State after:
case intro.hmotive
α : Type u_1
v x : α
L : List α
hL✝ : ↑L = {x}.val
hL : L = [x]
⊢ (match L, hL✝ with
      | [], _hL => ⋯.elim
      | x_1 :: tail, _hL => x_1) =
      v ↔
    x = v

State before:
case intro.hmotive
α : Type u_1
v x : α
L : List α
hL✝ : ↑L = {x}.val
hL : L = [x]
⊢ (match L, hL✝ with
      | [], _hL => ⋯.elim
      | x_1 :: tail, _hL => x_1) =
      v ↔
    x = v
Tactic:
cases hL
State after:
case intro.hmotive.refl
α : Type u_1
v x : α
hL : ↑[x] = {x}.val
⊢ (match [x], hL with
      | [], _hL => ⋯.elim
      | x_1 :: tail, _hL => x_1) =
      v ↔
    x = v

State before:
case intro.hmotive.refl
α : Type u_1
v x : α
hL : ↑[x] = {x}.val
⊢ (match [x], hL with
      | [], _hL => ⋯.elim
      | x_1 :: tail, _hL => x_1) =
      v ↔
    x = v
Tactic:
simp
State after:
no goals