finset_induction_bug.lean:30:23: error:invalid 'rewrite' tactic, step produced type incorrect term, details: type mismatch at application
  @subtype.tag (list A) (@nodup A) x nodup_al'
term
  nodup_al'
has type
  @nodup A (@cons A a l')
but is expected to have type
  @nodup A x
rewrite step failed using pattern
  @cons A_1 a_1 l'_1
proof state:
A : Type,
h : decidable_eq A,
P : finset A → Prop,
H1 : P (@empty A),
H2 : ∀ ⦃s⦄ {a}, not (@mem A a s) → P s → P (@insert A h a s),
s : finset A,
u : nodup_list A,
l : list A,
a : A,
l' : list A,
IH :
  ∀ has_property,
    P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) l' has_property)),
nodup_al' : @nodup A (@cons A a l'),
anl' : not (@list.mem A a l'),
H3 : @eq (list A) (@list.insert A (λ a b, h a b) a l') (@cons A a l'),
nodup_l' : @nodup A l',
P_l' : P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) l' nodup_l')),
H4 :
  P
    (@insert A (λ a b, h a b) a
       (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) l' nodup_l')))
⊢ P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) (@cons A a l') nodup_al'))
finset_induction_bug.lean:30:45: error: don't know how to synthesize placeholder
A : Type,
h : decidable_eq A,
P : finset A → Prop,
H1 : P (@empty A),
H2 : ∀ ⦃s⦄ {a}, not (@mem A a s) → P s → P (@insert A h a s),
s : finset A,
u : nodup_list A,
l : list A,
a : A,
l' : list A,
IH :
  ∀ has_property,
    P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) l' has_property)),
nodup_al' : @nodup A (@cons A a l'),
anl' : not (@list.mem A a l'),
H3 : @eq (list A) (@list.insert A (λ a b, h a b) a l') (@cons A a l'),
nodup_l' : @nodup A l',
P_l' : P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) l' nodup_l')),
H4 :
  P
    (@insert A (λ a b, h a b) a
       (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) l' nodup_l')))
⊢ P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) (@cons A a l') nodup_al'))
finset_induction_bug.lean:16:5: error: failed to add declaration 'finset.induction₂' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term
  λ A h P H1 H2 s,
    @quot.induction_on … … P s
      (λ u,
         @subtype.destruct … … … u
           (λ l,
              @list.induction_on A … l …
                (λ a l' IH nodup_al',
                   have anl' : …, from …,
                   have H3 : …, from …,
                   have nodup_l' : …, from …,
                   have P_l' : …, from …,
                   ?M_1 …)))
finset_induction_bug.lean:30:49: error: invalid end of module, expecting 'end'