Theorem: Fintype.elim_elems_eq_forall
Proof state before:
V : Type u_1
β : Type u_2
inst✝ : Fintype V
f : (L : List V) → (∀ (v : V), v ∈ L) → List.Nodup L → β
h :
  ∀ (L1 : List V) (h1 : ∀ (v : V), v ∈ L1) (h11 : List.Nodup L1) (L2 : List V) (h2 : ∀ (v : V), v ∈ L2)
    (h22 : List.Nodup L2), f L1 h1 h11 = f L2 h2 h22
C : Prop
h' : ∀ (L : List V) (h1 : ∀ (v : V), v ∈ L) (h2 : List.Nodup L), elim_elems f h = f L h1 h2 → C
L : List ?m.10905
hL : ↑L = ?m.10907
hM : Multiset.elim ?m.10907 ?m.10908 ?m.10909 = ?m.10908 L hL
⊢ C

V : Type u_1
β : Type u_2
inst✝ : Fintype V
f : (L : List V) → (∀ (v : V), v ∈ L) → List.Nodup L → β
h :
  ∀ (L1 : List V) (h1 : ∀ (v : V), v ∈ L1) (h11 : List.Nodup L1) (L2 : List V) (h2 : ∀ (v : V), v ∈ L2)
    (h22 : List.Nodup L2), f L1 h1 h11 = f L2 h2 h22
C : Prop
h' : ∀ (L : List V) (h1 : ∀ (v : V), v ∈ L) (h2 : List.Nodup L), elim_elems f h = f L h1 h2 → C
⊢ Type ?u.10903

V : Type u_1
β : Type u_2
inst✝ : Fintype V
f : (L : List V) → (∀ (v : V), v ∈ L) → List.Nodup L → β
h :
  ∀ (L1 : List V) (h1 : ∀ (v : V), v ∈ L1) (h11 : List.Nodup L1) (L2 : List V) (h2 : ∀ (v : V), v ∈ L2)
    (h22 : List.Nodup L2), f L1 h1 h11 = f L2 h2 h22
C : Prop
h' : ∀ (L : List V) (h1 : ∀ (v : V), v ∈ L) (h2 : List.Nodup L), elim_elems f h = f L h1 h2 → C
⊢ Type ?u.10904

V : Type u_1
β : Type u_2
inst✝ : Fintype V
f : (L : List V) → (∀ (v : V), v ∈ L) → List.Nodup L → β
h :
  ∀ (L1 : List V) (h1 : ∀ (v : V), v ∈ L1) (h11 : List.Nodup L1) (L2 : List V) (h2 : ∀ (v : V), v ∈ L2)
    (h22 : List.Nodup L2), f L1 h1 h11 = f L2 h2 h22
C : Prop
h' : ∀ (L : List V) (h1 : ∀ (v : V), v ∈ L) (h2 : List.Nodup L), elim_elems f h = f L h1 h2 → C
⊢ Multiset ?m.10905

V : Type u_1
β : Type u_2
inst✝ : Fintype V
f : (L : List V) → (∀ (v : V), v ∈ L) → List.Nodup L → β
h :
  ∀ (L1 : List V) (h1 : ∀ (v : V), v ∈ L1) (h11 : List.Nodup L1) (L2 : List V) (h2 : ∀ (v : V), v ∈ L2)
    (h22 : List.Nodup L2), f L1 h1 h11 = f L2 h2 h22
C : Prop
h' : ∀ (L : List V) (h1 : ∀ (v : V), v ∈ L) (h2 : List.Nodup L), elim_elems f h = f L h1 h2 → C
⊢ (L : List ?m.10905) → ↑L = ?m.10907 → ?m.10906

V : Type u_1
β : Type u_2
inst✝ : Fintype V
f : (L : List V) → (∀ (v : V), v ∈ L) → List.Nodup L → β
h :
  ∀ (L1 : List V) (h1 : ∀ (v : V), v ∈ L1) (h11 : List.Nodup L1) (L2 : List V) (h2 : ∀ (v : V), v ∈ L2)
    (h22 : List.Nodup L2), f L1 h1 h11 = f L2 h2 h22
C : Prop
h' : ∀ (L : List V) (h1 : ∀ (v : V), v ∈ L) (h2 : List.Nodup L), elim_elems f h = f L h1 h2 → C
⊢ ∀ (a b : List ?m.10905) (ha : ↑a = ?m.10907) (hb : ↑b = ?m.10907), ?m.10908 a ha = ?m.10908 b hb
Tactic:
apply h'
Proof state after:
case a
V : Type u_1
β : Type u_2
inst✝ : Fintype V
f : (L : List V) → (∀ (v : V), v ∈ L) → List.Nodup L → β
h :
  ∀ (L1 : List V) (h1 : ∀ (v : V), v ∈ L1) (h11 : List.Nodup L1) (L2 : List V) (h2 : ∀ (v : V), v ∈ L2)
    (h22 : List.Nodup L2), f L1 h1 h11 = f L2 h2 h22
C : Prop
h' : ∀ (L : List V) (h1 : ∀ (v : V), v ∈ L) (h2 : List.Nodup L), elim_elems f h = f L h1 h2 → C
L : List ?m.10905
hL : ↑L = ?m.10907
hM : Multiset.elim ?m.10907 ?m.10908 ?m.10909 = ?m.10908 L hL
⊢ elim_elems f h = f ?L ?h1 ?h2

case L
V : Type u_1
β : Type u_2
inst✝ : Fintype V
f : (L : List V) → (∀ (v : V), v ∈ L) → List.Nodup L → β
h :
  ∀ (L1 : List V) (h1 : ∀ (v : V), v ∈ L1) (h11 : List.Nodup L1) (L2 : List V) (h2 : ∀ (v : V), v ∈ L2)
    (h22 : List.Nodup L2), f L1 h1 h11 = f L2 h2 h22
C : Prop
h' : ∀ (L : List V) (h1 : ∀ (v : V), v ∈ L) (h2 : List.Nodup L), elim_elems f h = f L h1 h2 → C
L : List ?m.10905
hL : ↑L = ?m.10907
hM : Multiset.elim ?m.10907 ?m.10908 ?m.10909 = ?m.10908 L hL
⊢ List V

case h1
V : Type u_1
β : Type u_2
inst✝ : Fintype V
f : (L : List V) → (∀ (v : V), v ∈ L) → List.Nodup L → β
h :
  ∀ (L1 : List V) (h1 : ∀ (v : V), v ∈ L1) (h11 : List.Nodup L1) (L2 : List V) (h2 : ∀ (v : V), v ∈ L2)
    (h22 : List.Nodup L2), f L1 h1 h11 = f L2 h2 h22
C : Prop
h' : ∀ (L : List V) (h1 : ∀ (v : V), v ∈ L) (h2 : List.Nodup L), elim_elems f h = f L h1 h2 → C
L : List ?m.10905
hL : ↑L = ?m.10907
hM : Multiset.elim ?m.10907 ?m.10908 ?m.10909 = ?m.10908 L hL
⊢ ∀ (v : V), v ∈ ?L

case h2
V : Type u_1
β : Type u_2
inst✝ : Fintype V
f : (L : List V) → (∀ (v : V), v ∈ L) → List.Nodup L → β
h :
  ∀ (L1 : List V) (h1 : ∀ (v : V), v ∈ L1) (h11 : List.Nodup L1) (L2 : List V) (h2 : ∀ (v : V), v ∈ L2)
    (h22 : List.Nodup L2), f L1 h1 h11 = f L2 h2 h22
C : Prop
h' : ∀ (L : List V) (h1 : ∀ (v : V), v ∈ L) (h2 : List.Nodup L), elim_elems f h = f L h1 h2 → C
L : List ?m.10905
hL : ↑L = ?m.10907
hM : Multiset.elim ?m.10907 ?m.10908 ?m.10909 = ?m.10908 L hL
⊢ List.Nodup ?L

V : Type u_1
β : Type u_2
inst✝ : Fintype V
f : (L : List V) → (∀ (v : V), v ∈ L) → List.Nodup L → β
h :
  ∀ (L1 : List V) (h1 : ∀ (v : V), v ∈ L1) (h11 : List.Nodup L1) (L2 : List V) (h2 : ∀ (v : V), v ∈ L2)
    (h22 : List.Nodup L2), f L1 h1 h11 = f L2 h2 h22
C : Prop
h' : ∀ (L : List V) (h1 : ∀ (v : V), v ∈ L) (h2 : List.Nodup L), elim_elems f h = f L h1 h2 → C
⊢ Type ?u.10903

V : Type u_1
β : Type u_2
inst✝ : Fintype V
f : (L : List V) → (∀ (v : V), v ∈ L) → List.Nodup L → β
h :
  ∀ (L1 : List V) (h1 : ∀ (v : V), v ∈ L1) (h11 : List.Nodup L1) (L2 : List V) (h2 : ∀ (v : V), v ∈ L2)
    (h22 : List.Nodup L2), f L1 h1 h11 = f L2 h2 h22
C : Prop
h' : ∀ (L : List V) (h1 : ∀ (v : V), v ∈ L) (h2 : List.Nodup L), elim_elems f h = f L h1 h2 → C
⊢ Type ?u.10904

V : Type u_1
β : Type u_2
inst✝ : Fintype V
f : (L : List V) → (∀ (v : V), v ∈ L) → List.Nodup L → β
h :
  ∀ (L1 : List V) (h1 : ∀ (v : V), v ∈ L1) (h11 : List.Nodup L1) (L2 : List V) (h2 : ∀ (v : V), v ∈ L2)
    (h22 : List.Nodup L2), f L1 h1 h11 = f L2 h2 h22
C : Prop
h' : ∀ (L : List V) (h1 : ∀ (v : V), v ∈ L) (h2 : List.Nodup L), elim_elems f h = f L h1 h2 → C
⊢ Multiset ?m.10905

V : Type u_1
β : Type u_2
inst✝ : Fintype V
f : (L : List V) → (∀ (v : V), v ∈ L) → List.Nodup L → β
h :
  ∀ (L1 : List V) (h1 : ∀ (v : V), v ∈ L1) (h11 : List.Nodup L1) (L2 : List V) (h2 : ∀ (v : V), v ∈ L2)
    (h22 : List.Nodup L2), f L1 h1 h11 = f L2 h2 h22
C : Prop
h' : ∀ (L : List V) (h1 : ∀ (v : V), v ∈ L) (h2 : List.Nodup L), elim_elems f h = f L h1 h2 → C
⊢ (L : List ?m.10905) → ↑L = ?m.10907 → ?m.10906

V : Type u_1
β : Type u_2
inst✝ : Fintype V
f : (L : List V) → (∀ (v : V), v ∈ L) → List.Nodup L → β
h :
  ∀ (L1 : List V) (h1 : ∀ (v : V), v ∈ L1) (h11 : List.Nodup L1) (L2 : List V) (h2 : ∀ (v : V), v ∈ L2)
    (h22 : List.Nodup L2), f L1 h1 h11 = f L2 h2 h22
C : Prop
h' : ∀ (L : List V) (h1 : ∀ (v : V), v ∈ L) (h2 : List.Nodup L), elim_elems f h = f L h1 h2 → C
⊢ ∀ (a b : List ?m.10905) (ha : ↑a = ?m.10907) (hb : ↑b = ?m.10907), ?m.10908 a ha = ?m.10908 b hb